Computer Aided Verification [[electronic resource] ] : 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings / / edited by Ganesh Gopalakrishnan, Shaz Qadeer |
Edizione | [1st ed. 2011.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
Descrizione fisica | 1 online resource (XV, 763 p. 180 illus., 46 illus. in color.) |
Disciplina | 005.1015113 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Software engineering Compilers (Computer programs) Machine theory Computer programming Artificial intelligence Computer Science Logic and Foundations of Programming Software Engineering Compilers and Interpreters Formal Languages and Automata Theory Programming Techniques Artificial Intelligence |
ISBN | 3-642-22110-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996465714203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal methods in computer-aided design : second international conference, FMCAD '98, Palo Alto, CA, USA, November 4-6, 1998 : proceedings / / Ganesh Gopalakrishnan, Phillip Windley (editors) |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin : , : Springer, , [1998] |
Descrizione fisica | 1 online resource (X, 538 p.) |
Disciplina | 621.392 |
Collana | Lecture notes in computer science |
Soggetto topico |
Digital integrated circuits - Computer-aided design
Computer engineering - Computer-aided design Integrated circuits - Verification Automatic theorem proving Formal methods (Computer science) |
ISBN | 3-540-49519-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification -- Reducing Manual Abstraction in Formal Verification of Out- of- Order Execution -- Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking -- Solving Bit-Vector Equations -- The Formal Design of 1M-Gate ASICs -- Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations -- A Tutorial on Stålmarck’s Proof Procedure for Propositional Logic -- Almana: A BDD Minimization Tool Integrating Heuristic and RewritingMethods -- Bisimulation Minimization in an Automata-Theoretic Verification Framework -- Automatic Verification of Mixed-Level Logic Circuits -- A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk -- Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints -- Using MTBDDs for Composition and Model Checking of Real-Time Systems -- Formal Methods in CAD from an Industrial Perspective -- A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool -- Combined Formal Post- and Presynthesis Verification in High Level Synthesis -- Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem -- A Performance Study of BDD-Based Model Checking -- Symbolic Model Checking Visualization -- Input Elimination and Abstraction in Model Checking -- Symbolic Simulation of the JEM1 Microprocessor -- Symbolic Simulation: An ACL2 Approach -- Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study -- Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification -- Formally Verifying Data and Control with Weak Reachability Invariants -- Generalized Reversible Rules -- An Assume-Guarantee Rule for Checking Simulation -- Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared -- An Instruction Set Process Calculus -- Techniques for Implicit State Enumeration of EFSMs -- Model Checking on Product Structures -- BDDNOW: A Parallel BDD Package -- Model Checking VHDL with CV -- Alexandria: A Tool for Hierarchical Verification -- PV: An Explicit Enumeration Model-Checker. |
Record Nr. | UNINA-9910143467903321 |
Berlin : , : Springer, , [1998] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Formal methods in computer-aided design : second international conference, FMCAD '98, Palo Alto, CA, USA, November 4-6, 1998 : proceedings / / Ganesh Gopalakrishnan, Phillip Windley (editors) |
Edizione | [1st ed. 1998.] |
Pubbl/distr/stampa | Berlin : , : Springer, , [1998] |
Descrizione fisica | 1 online resource (X, 538 p.) |
Disciplina | 621.392 |
Collana | Lecture notes in computer science |
Soggetto topico |
Digital integrated circuits - Computer-aided design
Computer engineering - Computer-aided design Integrated circuits - Verification Automatic theorem proving Formal methods (Computer science) |
ISBN | 3-540-49519-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification -- Reducing Manual Abstraction in Formal Verification of Out- of- Order Execution -- Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking -- Solving Bit-Vector Equations -- The Formal Design of 1M-Gate ASICs -- Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations -- A Tutorial on Stålmarck’s Proof Procedure for Propositional Logic -- Almana: A BDD Minimization Tool Integrating Heuristic and RewritingMethods -- Bisimulation Minimization in an Automata-Theoretic Verification Framework -- Automatic Verification of Mixed-Level Logic Circuits -- A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk -- Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints -- Using MTBDDs for Composition and Model Checking of Real-Time Systems -- Formal Methods in CAD from an Industrial Perspective -- A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool -- Combined Formal Post- and Presynthesis Verification in High Level Synthesis -- Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem -- A Performance Study of BDD-Based Model Checking -- Symbolic Model Checking Visualization -- Input Elimination and Abstraction in Model Checking -- Symbolic Simulation of the JEM1 Microprocessor -- Symbolic Simulation: An ACL2 Approach -- Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study -- Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification -- Formally Verifying Data and Control with Weak Reachability Invariants -- Generalized Reversible Rules -- An Assume-Guarantee Rule for Checking Simulation -- Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared -- An Instruction Set Process Calculus -- Techniques for Implicit State Enumeration of EFSMs -- Model Checking on Product Structures -- BDDNOW: A Parallel BDD Package -- Model Checking VHDL with CV -- Alexandria: A Tool for Hierarchical Verification -- PV: An Explicit Enumeration Model-Checker. |
Record Nr. | UNISA-996465910703316 |
Berlin : , : Springer, , [1998] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging |
Autore | Gopalakrishnan Ganesh |
Pubbl/distr/stampa | [Place of publication not identified], : Association for Computing Machinery, 2009 |
Descrizione fisica | 1 online resource (99 p.;) |
Collana | ACM Conferences |
Soggetto topico | Information Technology - Computer Science (Hardware & Networks) |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Altri titoli varianti | PADTAD '09 |
Record Nr. | UNINA-9910376254003321 |
Gopalakrishnan Ganesh | ||
[Place of publication not identified], : Association for Computing Machinery, 2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|