Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Computer Aided Verification [[electronic resource] ] : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28-July 2, 1998, Proceedings / / edited by Alan J. Hu, Moshe Y. Vardi
| Computer Aided Verification [[electronic resource] ] : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28-July 2, 1998, Proceedings / / edited by Alan J. Hu, Moshe Y. Vardi |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (X, 552 p.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computers Computer logic Mathematical logic Logic design Software Engineering/Programming and Operating Systems Theory of Computation Logics and Meanings of Programs Software Engineering Mathematical Logic and Formal Languages Logic Design |
| ISBN | 3-540-69339-4 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Synchronous programming of reactive systems -- Ten years of partial order reduction -- An ACL2 proof of write invalidate cache coherence -- Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle -- A role for theorem proving in multi-processor design -- A formal method experience at secure computing corporation -- Formal methods in an industrial environment -- On checking model checkers -- Finite-state analysis of security protocols -- Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols -- Verifying systems with infinite but regular state spaces -- Formal verification of out-of-order execution using incremental flushing -- Verification of an implementation of Tomasulo's algorithm by compositional model checking -- Decomposing the proof of correctness of pipelined microprocessors -- Processor verification with precise exceptions and speculative execution -- Symmetry reductions in model checking -- Structural symmetry and model checking -- Using magnetic disk instead of main memory in the Mur ? verifier -- On-the-fly model checking of RCTL formulas -- From pre-historic to post-modern symbolic model checking -- Model checking LTL using net unforldings -- Model checking for a first-order temporal logic using multiway decision graphs -- On the limitations of ordered representations of functions -- BDD based procedures for a theory of equality with uninterpreted functions -- Computing reachable control states of systems modeled with uninterpreted functions and infinite memory -- Multiple counters automata, safety analysis and presburger arithmetic -- A comparison of Presburger engines for EFSM reachability -- Generating finite-state abstractions of reactive systems using decision procedures -- On-the-fly analysis of systems with unbounded, lossy FIFO channels -- Computing abstractions of infinite state systems compositionally and automatically -- Normed simulations -- An experiment in parallelizing an application using formal methods -- Efficient symbolic detection of global properties in distributed systems -- A machine-checked proof of the optimality of a real-time scheduling policy -- A general approach to partial order reductions in symbolic verification -- Correctness of the concurrent approach to symbolic verification of interleaved models -- Verification of timed systems using POSETs -- Mechanising BAN Kerberos by the inductive method -- Protocol verification in Nuprl -- You assume, we guarantee: Methodology and case studies -- Verification of a parameterized bus arbitration protocol -- The ‘test model-checking’ approach to the verification of formal memory models of multiprocessors -- Design constraints in symbolic model checking -- Verification of floating-point adders -- Xeve, an Esterel verification environment -- InVeSt : A tool for the verification of invariants -- Verifying mobile processes in the HAL environment -- MONA 1.x: New techniques for WS1S and WS2S -- MOCHA: Modularity in model checking -- SCR: A toolset for specifying and analyzing software requirements -- A toolset for message sequence charts -- Real-time verification of Statemate designs -- Optikron: A tool suite for enhancing model-checking of real-time systems -- Kronos: A model-checking tool for real-time systems. |
| Record Nr. | UNINA-9910144909603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Aided Verification [[electronic resource] ] : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28-July 2, 1998, Proceedings / / edited by Alan J. Hu, Moshe Y. Vardi
| Computer Aided Verification [[electronic resource] ] : 10th International Conference, CAV'98, Vancouver, BC, Canada, June 28-July 2, 1998, Proceedings / / edited by Alan J. Hu, Moshe Y. Vardi |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 |
| Descrizione fisica | 1 online resource (X, 552 p.) |
| Disciplina | 005.1 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computers Computer logic Mathematical logic Logic design Software Engineering/Programming and Operating Systems Theory of Computation Logics and Meanings of Programs Software Engineering Mathematical Logic and Formal Languages Logic Design |
| ISBN | 3-540-69339-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Synchronous programming of reactive systems -- Ten years of partial order reduction -- An ACL2 proof of write invalidate cache coherence -- Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle -- A role for theorem proving in multi-processor design -- A formal method experience at secure computing corporation -- Formal methods in an industrial environment -- On checking model checkers -- Finite-state analysis of security protocols -- Integrating proof-based and model-checking techniques for the formal verification of cryptographic protocols -- Verifying systems with infinite but regular state spaces -- Formal verification of out-of-order execution using incremental flushing -- Verification of an implementation of Tomasulo's algorithm by compositional model checking -- Decomposing the proof of correctness of pipelined microprocessors -- Processor verification with precise exceptions and speculative execution -- Symmetry reductions in model checking -- Structural symmetry and model checking -- Using magnetic disk instead of main memory in the Mur ? verifier -- On-the-fly model checking of RCTL formulas -- From pre-historic to post-modern symbolic model checking -- Model checking LTL using net unforldings -- Model checking for a first-order temporal logic using multiway decision graphs -- On the limitations of ordered representations of functions -- BDD based procedures for a theory of equality with uninterpreted functions -- Computing reachable control states of systems modeled with uninterpreted functions and infinite memory -- Multiple counters automata, safety analysis and presburger arithmetic -- A comparison of Presburger engines for EFSM reachability -- Generating finite-state abstractions of reactive systems using decision procedures -- On-the-fly analysis of systems with unbounded, lossy FIFO channels -- Computing abstractions of infinite state systems compositionally and automatically -- Normed simulations -- An experiment in parallelizing an application using formal methods -- Efficient symbolic detection of global properties in distributed systems -- A machine-checked proof of the optimality of a real-time scheduling policy -- A general approach to partial order reductions in symbolic verification -- Correctness of the concurrent approach to symbolic verification of interleaved models -- Verification of timed systems using POSETs -- Mechanising BAN Kerberos by the inductive method -- Protocol verification in Nuprl -- You assume, we guarantee: Methodology and case studies -- Verification of a parameterized bus arbitration protocol -- The ‘test model-checking’ approach to the verification of formal memory models of multiprocessors -- Design constraints in symbolic model checking -- Verification of floating-point adders -- Xeve, an Esterel verification environment -- InVeSt : A tool for the verification of invariants -- Verifying mobile processes in the HAL environment -- MONA 1.x: New techniques for WS1S and WS2S -- MOCHA: Modularity in model checking -- SCR: A toolset for specifying and analyzing software requirements -- A toolset for message sequence charts -- Real-time verification of Statemate designs -- Optikron: A tool suite for enhancing model-checking of real-time systems -- Kronos: A model-checking tool for real-time systems. |
| Record Nr. | UNISA-996466084303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Methods in Computer-Aided Design [[electronic resource] ] : 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings / / edited by Alan J. Hu, Andrew K. Martin
| Formal Methods in Computer-Aided Design [[electronic resource] ] : 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings / / edited by Alan J. Hu, Andrew K. Martin |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 448 p.) |
| Disciplina | 621.39/5 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer-aided engineering
Computer hardware Software engineering Computer logic Mathematical logic Artificial intelligence Computer-Aided Engineering (CAD, CAE) and Design Computer Hardware Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN | 3-540-30494-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Challenges in System-Level Design -- Generating Fast Multipliers Using Clever Circuits -- Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques -- A Methodology for the Formal Verification of FFT Algorithms in HOL -- A Functional Approach to the Formal Specification of Networks on Chip -- Proof Styles in Operational Semantics -- Integrating Reasoning About Ordinal Arithmetic into ACL2 -- Combining Equivalence Verification and Completion Functions -- Synchronization-at-Retirement for Pipeline Verification -- Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs -- Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders -- Scalable Automated Verification via Expert-System Guided Transformations -- Simple Yet Efficient Improvements of SAT Based Bounded Model Checking -- Simple Bounded LTL Model Checking -- QuBE++: An Efficient QBF Solver -- Bounded Probabilistic Model Checking with the Mur? Verifier -- Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States -- Bounded Verification of Past LTL -- A Hybrid of Counterexample-Based and Proof-Based Abstraction -- Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis -- Approximate Symbolic Model Checking for Incomplete Designs -- Extending Extended Vacuity -- Parameterized Vacuity -- An Operational Semantics for Weak PSL -- Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking -- Bloom Filters in Probabilistic Verification -- A Simple Method for Parameterized Verification of Cache Coherence Protocols -- A Partitioning Methodology for BDD-Based Verification -- Invariant Checking Combining Forward and Backward Traversal -- Variable Reuse for Efficient Image Computation. |
| Record Nr. | UNISA-996465493903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Methods in Computer-Aided Design : 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings / / edited by Alan J. Hu, Andrew K. Martin
| Formal Methods in Computer-Aided Design : 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings / / edited by Alan J. Hu, Andrew K. Martin |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 448 p.) |
| Disciplina | 621.39/5 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer-aided engineering
Computer hardware Software engineering Computer logic Mathematical logic Artificial intelligence Computer-Aided Engineering (CAD, CAE) and Design Computer Hardware Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN | 3-540-30494-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Challenges in System-Level Design -- Generating Fast Multipliers Using Clever Circuits -- Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques -- A Methodology for the Formal Verification of FFT Algorithms in HOL -- A Functional Approach to the Formal Specification of Networks on Chip -- Proof Styles in Operational Semantics -- Integrating Reasoning About Ordinal Arithmetic into ACL2 -- Combining Equivalence Verification and Completion Functions -- Synchronization-at-Retirement for Pipeline Verification -- Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs -- Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders -- Scalable Automated Verification via Expert-System Guided Transformations -- Simple Yet Efficient Improvements of SAT Based Bounded Model Checking -- Simple Bounded LTL Model Checking -- QuBE++: An Efficient QBF Solver -- Bounded Probabilistic Model Checking with the Mur? Verifier -- Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States -- Bounded Verification of Past LTL -- A Hybrid of Counterexample-Based and Proof-Based Abstraction -- Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis -- Approximate Symbolic Model Checking for Incomplete Designs -- Extending Extended Vacuity -- Parameterized Vacuity -- An Operational Semantics for Weak PSL -- Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking -- Bloom Filters in Probabilistic Verification -- A Simple Method for Parameterized Verification of Cache Coherence Protocols -- A Partitioning Methodology for BDD-Based Verification -- Invariant Checking Combining Forward and Backward Traversal -- Variable Reuse for Efficient Image Computation. |
| Record Nr. | UNINA-9910144338003321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Hardware and Software: Verification and Testing [[electronic resource] ] : 4th International Haifa Verification Conference, HVC 2008, Haifa, Israel, October 27-30, 2008, Revised Selected Papers / / edited by Hana Chockler, Alan J. Hu
| Hardware and Software: Verification and Testing [[electronic resource] ] : 4th International Haifa Verification Conference, HVC 2008, Haifa, Israel, October 27-30, 2008, Revised Selected Papers / / edited by Hana Chockler, Alan J. Hu |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (XII, 215 p.) |
| Disciplina | 005.1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters |
| ISBN | 3-642-01702-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Section 1: Invited Talks -- Hazards of Verification -- Automata-Theoretic Model Checking Revisited -- Proofs, Interpolants, and Relevance Heuristics -- Is Verification Getting Too Complex? -- Can Mutation Analysis Help Fix Our Broken Coverage Metrics? -- Practical Considerations Concerning HL-to -RT Equivalence Checking -- Section 2: Regular Papers -- A Framework for Inherent Vacuity -- A Meta Heuristic for Effectively Detecting Concurrency Errors -- A Uniform Approach to Three-Valued Semantics for ?-Calculus on Abstractions of Hybrid Automata -- Automatic Boosting of Cross-Product Coverage Using Bayesian Networks -- Efficient Decision Procedure for Bounded Integer Non-linear Operations Using SMT( ) -- Evaluating Workloads Using Comparative Functional Coverage -- Iterative Delta Debugging -- Linear-Time Reductions of Resolution Proofs -- Significant Diagnostic Counterexamples in Probabilistic Model Checking -- Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order ????? Modulator -- Structural Contradictions -- Synthesizing Test Models from Test Cases -- Section 3: Tool Papers -- d-TSR: Parallelizing SMT-Based BMC Using Tunnels over a Distributed Framework -- Progress in Automated Software Defect Prediction -- SeeCode – A Code Review Plug-in for Eclipse -- User-Friendly Model Checking: Automatically Configuring Algorithms with RuleBase/PE. |
| Record Nr. | UNISA-996466029203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||