Automated Technology for Verification and Analysis [[electronic resource] ] : Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, Proceedings / / edited by Doron A. Peled, Yih-Kuen Tsay |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (XII, 508 p.) |
Disciplina | 620.00420285 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computer-aided engineering
Computer logic Computer communication systems Special purpose computers Software engineering Programming languages (Electronic computers) Computer-Aided Engineering (CAD, CAE) and Design Logics and Meanings of Programs Computer Communication Networks Special Purpose and Application-Based Systems Software Engineering Programming Languages, Compilers, Interpreters |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynote Speeches -- Ranking Abstraction as a Companion to Predicate Abstraction -- Termination and Invariance Analysis of Loops -- Some Perspectives of Infinite-State Verification -- Model Checking -- Verifying Very Large Industrial Circuits Using 100 Processes and Beyond -- A New Reachability Algorithm for Symmetric Multi-processor Architecture -- Comprehensive Verification Framework for Dependability of Self-optimizing Systems -- Exploiting Hub States in Automatic Verification -- Combined Methods -- An Approach for the Verification of SystemC Designs Using AsmL -- Decomposition-Based Verification of Cyclic Workflows -- Timed, Embedded, and Hybrid Systems (I) -- Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems -- Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach -- Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities -- Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems -- Abstraction and Reduction Techniques -- Selective Search in Bounded Model Checking of Reachability Properties -- Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming -- State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method -- Syntactical Colored Petri Nets Reductions -- Decidability and Complexity -- Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology -- A Static Analysis Using Tree Automata for XML Access Control -- Reasoning About Transfinite Sequences -- Semi-automatic Distributed Synthesis -- Established Formalisms and Standards -- A New Graph of Classes for the Preservation of Quantitative Temporal Constraints -- Comparison of Different Semantics for Time Petri Nets -- Introducing Dynamic Properties with Past Temporal Operators in the B Refinement -- Approximate Reachability for Dead Code Elimination in Esterel??? -- Compositional Verification and Games -- Synthesis of Interface Automata -- Multi-valued Model Checking Games -- Timed, Embedded, and Hybrid Systems (II) -- Model Checking Prioritized Timed Automata -- An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata -- Protocols Analysis, Case Studies, and Tools -- An EFSM-Based Intrusion Detection System for Ad Hoc Networks -- Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool -- Formal Construction and Verification of Home Service Robots: A Case Study -- Model Checking Real Time Java Using Java PathFinder -- Infinite-State and Parameterized Systems -- Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols -- Flat Acceleration in Symbolic Model Checking -- Flat Counter Automata Almost Everywhere!. |
Record Nr. | UNISA-996466222103316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Computer Aided Verification [[electronic resource] ] : 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings / / edited by Rajeev Alur, Doron A. Peled |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (XII, 536 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Software engineering Logic design Computer logic Mathematical logic Artificial intelligence Theory of Computation Software Engineering Logic Design Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
ISBN | 3-540-27813-3 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Rob Tristan Gerth: 1956–2003 -- Static Program Analysis via 3-Valued Logic -- Deductive Verification of Pipelined Machines Using First-Order Quantification -- A Formal Reduction for Lock-Free Parallel Algorithms -- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking -- Termination of Linear Programs -- Symbolic Model Checking of Non-regular Properties -- Proving More Properties with Bounded Model Checking -- Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings -- Using Interface Refinement to Integrate Formal Verification into the Design Cycle -- Indexed Predicate Discovery for Unbounded System Verification -- Range Allocation for Separation Logic -- An Experimental Evaluation of Ground Decision Procedures -- DPLL(T): Fast Decision Procedures -- Verifying ?-Regular Properties of Markov Chains -- Statistical Model Checking of Black-Box Probabilistic Systems -- Compositional Specification and Model Checking in GSTE -- GSTE Is Partitioned Model Checking -- Stuck-Free Conformance -- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors -- Functional Dependency for Verification Reduction -- Verification via Structure Simulation -- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures -- Abstraction-Based Satisfiability Solving of Presburger Arithmetic -- Widening Arithmetic Automata -- Why Model Checking Can Improve WCET Analysis -- Regular Model Checking for LTL(MSO) -- Image Computation in Infinite State Model Checking -- Abstract Regular Model Checking -- Global Model-Checking of Infinite-State Systems -- QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings -- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm -- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values -- Efficient Modeling of Embedded Memories in Bounded Model Checking -- Understanding Counterexamples with explain -- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement -- JNuke: Efficient Dynamic Analysis for Java -- The HiVy Tool Set -- ObsSlice: A Timed Automata Slicer Based on Observers -- The UCLID Decision Procedure -- MCK: Model Checking the Logic of Knowledge -- Zing: A Model Checker for Concurrent Software -- The Mec 5 Model-Checker -- PlayGame: A Platform for Diagnostic Games -- SAL 2 -- Formal Analysis of Java Programs in JavaFAN -- A Toolset for Modelling and Verification of GALS Systems -- WSAT: A Tool for Formal Analysis of Web Services -- CVC Lite: A New Implementation of the Cooperating Validity Checker -- CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking -- Mechanical Mathematical Methods for Microprocessor Verification. |
Record Nr. | UNISA-996465724703316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Computer Aided Verification : 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings / / edited by Rajeev Alur, Doron A. Peled |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (XII, 536 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Software engineering Logic design Computer logic Logic, Symbolic and mathematical Artificial intelligence Theory of Computation Software Engineering Logic Design Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
ISBN | 3-540-27813-3 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Rob Tristan Gerth: 1956–2003 -- Static Program Analysis via 3-Valued Logic -- Deductive Verification of Pipelined Machines Using First-Order Quantification -- A Formal Reduction for Lock-Free Parallel Algorithms -- An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking -- Termination of Linear Programs -- Symbolic Model Checking of Non-regular Properties -- Proving More Properties with Bounded Model Checking -- Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings -- Using Interface Refinement to Integrate Formal Verification into the Design Cycle -- Indexed Predicate Discovery for Unbounded System Verification -- Range Allocation for Separation Logic -- An Experimental Evaluation of Ground Decision Procedures -- DPLL(T): Fast Decision Procedures -- Verifying ?-Regular Properties of Markov Chains -- Statistical Model Checking of Black-Box Probabilistic Systems -- Compositional Specification and Model Checking in GSTE -- GSTE Is Partitioned Model Checking -- Stuck-Free Conformance -- Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors -- Functional Dependency for Verification Reduction -- Verification via Structure Simulation -- Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures -- Abstraction-Based Satisfiability Solving of Presburger Arithmetic -- Widening Arithmetic Automata -- Why Model Checking Can Improve WCET Analysis -- Regular Model Checking for LTL(MSO) -- Image Computation in Infinite State Model Checking -- Abstract Regular Model Checking -- Global Model-Checking of Infinite-State Systems -- QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings -- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm -- Automatic Verification of Sequential Consistency for Unbounded Addresses and Data Values -- Efficient Modeling of Embedded Memories in Bounded Model Checking -- Understanding Counterexamples with explain -- Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement -- JNuke: Efficient Dynamic Analysis for Java -- The HiVy Tool Set -- ObsSlice: A Timed Automata Slicer Based on Observers -- The UCLID Decision Procedure -- MCK: Model Checking the Logic of Knowledge -- Zing: A Model Checker for Concurrent Software -- The Mec 5 Model-Checker -- PlayGame: A Platform for Diagnostic Games -- SAL 2 -- Formal Analysis of Java Programs in JavaFAN -- A Toolset for Modelling and Verification of GALS Systems -- WSAT: A Tool for Formal Analysis of Web Services -- CVC Lite: A New Implementation of the Cooperating Validity Checker -- CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking -- Mechanical Mathematical Methods for Microprocessor Verification. |
Record Nr. | UNINA-9910767527303321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
![]() | ||
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 |
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 | ||
![]() | ||
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 |
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 networks
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 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Model Checking and Artificial Intelligence [[electronic resource] ] : 5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008, Revised Selected and Invited Papers / / edited by Doron A. Peled, Michael Wooldridge |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
Descrizione fisica | 1 online resource (VII, 189 p.) |
Disciplina | 006.3 |
Collana | Lecture Notes in Artificial Intelligence |
Soggetto topico |
Artificial intelligence
Programming languages (Electronic computers) Computer programming Software engineering Computer logic Mathematical logic Artificial Intelligence Programming Languages, Compilers, Interpreters Programming Techniques Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages |
Soggetto genere / forma | Kongress. |
ISBN | 3-642-00431-8 |
Classificazione |
DAT 325f
DAT 706f SS 4800 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Verifying Time and Communication Costs of Rule-Based Reasoners -- Solving ?-Calculus Parity Games by Symbolic Planning -- Verifying Robocup Teams -- Scaling Search with Pattern Databases -- Survey on Directed Model Checking -- Automated Testing of Planning Models -- Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic -- Model Checking Driven Heuristic Search for Correct Programs -- Experimental Evaluation of a Planning Language Suitable for Formal Verification -- Relaxation Refinement: A New Method to Generate Heuristic Functions -- Model Checking Strategic Equilibria. |
Record Nr. | UNISA-996465898003316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Runtime Verification [[electronic resource] ] : 9th International Workshop, RV 2009, Grenoble, France, June 26-28, 2009, Selected Papers / / edited by Saddek Bensalem, Doron A. Peled |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
Descrizione fisica | 1 online resource (VII, 203 p.) |
Disciplina | 005.1/17 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Computers Computer software—Reusability Programming languages (Electronic computers) Computer system failures Software Engineering Software Engineering/Programming and Operating Systems Theory of Computation Performance and Reliability Programming Languages, Compilers, Interpreters System Performance and Evaluation |
Soggetto genere / forma |
Grenobble (2009)
Grenoble (2009) Kongress. |
ISBN | 3-642-04694-0 |
Classificazione |
DAT 263f
DAT 325f SS 4800 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Rule Systems for Runtime Verification: A Short Tutorial -- Verification, Testing and Statistics -- Type-Separated Bytecode – Its Construction and Evaluation -- Runtime Verification of Safety-Progress Properties -- Monitor Circuits for LTL with Bounded and Unbounded Future -- State Joining and Splitting for the Symbolic Execution of Binaries -- The LIME Interface Specification Language and Runtime Monitoring Tool -- A Concurrency Testing Tool and Its Plug-Ins for Dynamic Analysis and Runtime Healing -- Bridging the Gap between Algebraic Specification and Object-Oriented Generic Programming -- Runtime Verification of C Memory Safety -- A Combined On-Line/Off-Line Framework for Black-Box Fault Diagnosis -- Hardware Supported Flexible Monitoring: Early Results -- DMaC: Distributed Monitoring and Checking. |
Record Nr. | UNISA-996465300203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Runtime Verification 9th International Workshop, RV 2009, Grenoble, France, June 26-28, 2009 ; Selected papers / / Saddek Bensalem, Doron A. Peled (eds.) |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin ; ; New York, NY, : Springer-Verlag, c2009 |
Descrizione fisica | 1 online resource (VII, 203 p.) |
Disciplina | 005.1/17 |
Altri autori (Persone) |
BensalemSaddeck
PeledDoron A |
Collana | Lecture notes in computer science |
Soggetto topico |
Computer software - Verification
Software engineering |
ISBN | 3-642-04694-0 |
Classificazione |
DAT 263f
DAT 325f SS 4800 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Rule Systems for Runtime Verification: A Short Tutorial -- Verification, Testing and Statistics -- Type-Separated Bytecode – Its Construction and Evaluation -- Runtime Verification of Safety-Progress Properties -- Monitor Circuits for LTL with Bounded and Unbounded Future -- State Joining and Splitting for the Symbolic Execution of Binaries -- The LIME Interface Specification Language and Runtime Monitoring Tool -- A Concurrency Testing Tool and Its Plug-Ins for Dynamic Analysis and Runtime Healing -- Bridging the Gap between Algebraic Specification and Object-Oriented Generic Programming -- Runtime Verification of C Memory Safety -- A Combined On-Line/Off-Line Framework for Black-Box Fault Diagnosis -- Hardware Supported Flexible Monitoring: Early Results -- DMaC: Distributed Monitoring and Checking. |
Record Nr. | UNINA-9910484723503321 |
Berlin ; ; New York, NY, : Springer-Verlag, c2009 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Time for Verification [[electronic resource] ] : Essays in Memory of Amir Pnueli / / edited by Zohar Manna, Doron A. Peled |
Edizione | [1st ed. 2010.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
Descrizione fisica | 1 online resource (VIII, 413 p. 113 illus.) |
Disciplina | 005.11 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer programming
Computer science Compilers (Computer programs) Machine theory Programming Techniques Theory of Computation Compilers and Interpreters Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming |
ISBN |
1-280-38730-0
9786613565228 3-642-13754-7 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Modal and Temporal Argumentation Networks -- Knowledge Based Scheduling of Distributed Systems -- Quantitative Simulation Games -- The Localization Reduction and Counterexample-Guided Abstraction Refinement -- A Scalable Segmented Decision Tree Abstract Domain -- Towards Component Based Design of Hybrid Systems: Safety and Stability -- Mildly Context-Sensitive Languages via Buffer Augmented Pregroup Grammars -- Inference Rules for Proving the Equivalence of Recursive Procedures -- Some Thoughts on the Semantics of Biocharts -- Unraveling a Card Trick -- An Automata-Theoretic Approach to Infinite-State Systems -- On the Krohn-Rhodes Cascaded Decomposition Theorem -- Temporal Verification of Reactive Systems: Response -- The Arrow of Time through the Lens of Computing -- What Is in a Step: New Perspectives on a Classical Question. |
Record Nr. | UNISA-996466435503316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Time for verification : essays in memory of Amir Pnueli / / Zohar Manna, Doron A. Peled (eds.) |
Edizione | [1st ed. 2010.] |
Pubbl/distr/stampa | Berlin, : Springer, 2010 |
Descrizione fisica | 1 online resource (VIII, 413 p. 113 illus.) |
Disciplina | 005.11 |
Altri autori (Persone) |
MannaZohar
PeledDoron A |
Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
Soggetto topico | Science - Methodology |
ISBN |
1-280-38730-0
9786613565228 3-642-13754-7 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Modal and Temporal Argumentation Networks -- Knowledge Based Scheduling of Distributed Systems -- Quantitative Simulation Games -- The Localization Reduction and Counterexample-Guided Abstraction Refinement -- A Scalable Segmented Decision Tree Abstract Domain -- Towards Component Based Design of Hybrid Systems: Safety and Stability -- Mildly Context-Sensitive Languages via Buffer Augmented Pregroup Grammars -- Inference Rules for Proving the Equivalence of Recursive Procedures -- Some Thoughts on the Semantics of Biocharts -- Unraveling a Card Trick -- An Automata-Theoretic Approach to Infinite-State Systems -- On the Krohn-Rhodes Cascaded Decomposition Theorem -- Temporal Verification of Reactive Systems: Response -- The Arrow of Time through the Lens of Computing -- What Is in a Step: New Perspectives on a Classical Question. |
Record Nr. | UNINA-9910484034403321 |
Berlin, : Springer, 2010 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|