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. | UNISA-996466084303316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1998 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 Logic, Symbolic and mathematical 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 | ||
| ||
Formal Techniques for Networked and Distributed Systems - FORTE 2002 [[electronic resource] ] : 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings / / edited by Doron A. Peled, Moshe Y. Vardi
| Formal Techniques for Networked and Distributed Systems - FORTE 2002 [[electronic resource] ] : 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings / / edited by Doron A. Peled, Moshe Y. Vardi |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (X, 374 p.) |
| Disciplina | 004.01/51 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer communication systems
Software engineering Operating systems (Computers) Computer logic Computer Communication Networks Software Engineering/Programming and Operating Systems Software Engineering Operating Systems Logics and Meanings of Programs |
| ISBN | 3-540-36135-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Encoding PAMR into (Timed) EFSMs -- Submodule Construction for Specifications with Input Assumptions and Output Guarantees -- Congruent Weak Conformance, a Partial Order among Processes -- Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures -- A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction -- Protocol Techniques for Testing Radiotherapy Accelerators -- System Test Synthesis from UML Models of Distributed Software -- Formal Test Purposes and the Validity of Test Cases -- Use of Logic to Describe Enhanced Communications Services -- A Formal Venture into Reliable Multicast Territory -- Modelling SIP Services Using Cress -- Verifying Reliable Data Transmission over UMTS Radio Interface with High Level Petri Nets -- Verifying Randomized Byzantine Agreement_ -- Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning -- Visual Specifications for Modular Reasoning about Asynchronous Systems -- Bounded Model Checking for Timed Systems -- C Wolf - A Toolset for Extracting Models from C Programs -- NTIF: A General Symbolic Model for Communicating Sequential Processes with Data -- Building Tools for LOTOS Symbolic Semantics in Maude -- From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata -- A Compositional Sweep-Line State Space Exploration Method -- On Combining the Persistent Sets Method with the Covering Steps Graph Method -- Innovative Verification Techniques Used in the Implementation of a Third-Generation 1.1GHz 64b Microprocessor -- Mechanical Translation of I/O Automaton Specifications into First-Order Logic -- Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams -- A Distributed Partial Order Reduction Algorithm. |
| Record Nr. | UNISA-996465498003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal Techniques for Networked and Distributed Systems - FORTE 2002 : 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings / / edited by Doron A. Peled, Moshe Y. Vardi
| Formal Techniques for Networked and Distributed Systems - FORTE 2002 : 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings / / edited by Doron A. Peled, Moshe Y. Vardi |
| Edizione | [1st ed. 2002.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
| Descrizione fisica | 1 online resource (X, 374 p.) |
| Disciplina | 004.01/51 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer communication systems
Software engineering Operating systems (Computers) Computer logic Computer Communication Networks Software Engineering/Programming and Operating Systems Software Engineering Operating Systems Logics and Meanings of Programs |
| ISBN | 3-540-36135-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Encoding PAMR into (Timed) EFSMs -- Submodule Construction for Specifications with Input Assumptions and Output Guarantees -- Congruent Weak Conformance, a Partial Order among Processes -- Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures -- A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction -- Protocol Techniques for Testing Radiotherapy Accelerators -- System Test Synthesis from UML Models of Distributed Software -- Formal Test Purposes and the Validity of Test Cases -- Use of Logic to Describe Enhanced Communications Services -- A Formal Venture into Reliable Multicast Territory -- Modelling SIP Services Using Cress -- Verifying Reliable Data Transmission over UMTS Radio Interface with High Level Petri Nets -- Verifying Randomized Byzantine Agreement_ -- Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning -- Visual Specifications for Modular Reasoning about Asynchronous Systems -- Bounded Model Checking for Timed Systems -- C Wolf - A Toolset for Extracting Models from C Programs -- NTIF: A General Symbolic Model for Communicating Sequential Processes with Data -- Building Tools for LOTOS Symbolic Semantics in Maude -- From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata -- A Compositional Sweep-Line State Space Exploration Method -- On Combining the Persistent Sets Method with the Covering Steps Graph Method -- Innovative Verification Techniques Used in the Implementation of a Third-Generation 1.1GHz 64b Microprocessor -- Mechanical Translation of I/O Automaton Specifications into First-Order Logic -- Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams -- A Distributed Partial Order Reduction Algorithm. |
| Record Nr. | UNINA-9910143884603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems
| Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems |
| Autore | Vardi Moshe Y |
| Pubbl/distr/stampa | [Place of publication not identified], : ACM, 1987 |
| Descrizione fisica | 1 online resource (363 pages) |
| Collana | ACM Conferences |
| Soggetto topico |
Engineering & Applied Sciences
Computer Science |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Proceedings of the sixth Association for Computing Machinery Special Interest Group on Algorithms and Computation Theory-Special Interest Group on Management of Data-Special Interest Group for Artificial Intelligence Symposium on Principles of Database Systems
PODS '87 Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems |
| Record Nr. | UNINA-9910376085003321 |
Vardi Moshe Y
|
||
| [Place of publication not identified], : ACM, 1987 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||