Computer Aided Verification [[electronic resource] ] : 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings / / edited by Werner Damm, Holger Hermanns |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XV, 562 p.) |
Disciplina | 006.3 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Software engineering Machine theory Artificial intelligence Logic design Theory of Computation Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence Logic Design |
ISBN | 3-540-73368-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Automatically Proving Program Termination -- A Mathematical Approach to RTL Verification -- Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? -- Invited Tutorials -- Algorithms for Interface Synthesis -- A Tutorial on Satisfiability Modulo Theories -- A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java -- Verification of Hybrid Systems -- Session I: Compositionality -- SAT-Based Compositional Verification Using Lazy Learning -- Local Proofs for Global Safety Properties -- Session II: Verification Process -- Low-Level Library Analysis and Summarization -- Verification Across Intellectual Property Boundaries -- Session III: Timed Synthesis and Games -- On Synthesizing Controllers from Bounded-Response Properties -- An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games -- UPPAAL-Tiga: Time for Playing Games! -- The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems -- Session IV: Infinitive State Verification -- Systematic Acceleration in Regular Model Checking -- Parameterized Verification of Infinite-State Processes with Global Conditions -- Session V: Tool Environment -- CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes -- jMoped: A Test Environment for Java Programs -- Hector: Software Model Checking with Cooperating Analysis Plugins -- The Why/Krakatoa/Caduceus Platform for Deductive Program Verification -- Session VI: Shapes -- Shape Analysis for Composite Data Structures -- Array Abstractions from Proofs -- Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures -- Revamping TVLA: Making Parametric Shape Analysis Competitive -- Session VII: Concurrent Program Verification -- Fast and Accurate Static Data-Race Detection for Concurrent Programs -- Parametric and Sliced Causality -- Spade: Verification of Multithreaded Dynamic and Recursive Programs -- Session VIII: Reactive Designs -- Anzu: A Tool for Property Synthesis -- RAT: A Tool for the Formal Analysis of Requirements -- Session IX: Parallelisation -- Parallelising Symbolic State-Space Generators -- I/O Efficient Accepting Cycle Detection -- Session X: Constraints and Decisions -- C32SAT: Checking C Expressions -- CVC3 -- BAT: The Bit-Level Analysis Tool -- LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals -- Session XI: Probabilistic Verification -- Three-Valued Abstraction for Continuous-Time Markov Chains -- Magnifying-Lens Abstraction for Markov Decision Processes -- Underapproximation for Model-Checking Based on Random Cryptographic Constructions -- Session XII: Abstraction -- Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra -- Structural Abstraction of Software Verification Conditions -- An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software -- Adaptive Symmetry Reduction -- Session XIII: Assume-Guarantee Reasoning -- From Liveness to Promptness -- Automated Assumption Generation for Compositional Verification -- Session XIV: Hybrid Systems -- Abstraction and Counterexample-Guided Construction of ?-Automata for Model Checking of Step-Discrete Linear Hybrid Models -- Test Coverage for Continuous and Hybrid Systems -- Hybrid Systems: From Verification to Falsification -- Session XV: Program Analysis -- Comparison Under Abstraction for Verifying Linearizability -- Leaping Loops in the Presence of Abstraction -- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis -- Session XVI: SAT and Decision Procedures -- A Decision Procedure for Bit-Vectors and Arrays -- Boolean Abstraction for Temporal Logic Satisfiability -- A Lazy and Layered SMT( ) Solver for Hard Industrial Verification Problems. |
Record Nr. | UNISA-996466098303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Computer Aided Verification : 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings / / edited by Werner Damm, Holger Hermanns |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XV, 562 p.) |
Disciplina | 006.3 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Software engineering Machine theory Artificial intelligence Logic design Theory of Computation Computer Science Logic and Foundations of Programming Software Engineering Formal Languages and Automata Theory Artificial Intelligence Logic Design |
ISBN | 3-540-73368-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Automatically Proving Program Termination -- A Mathematical Approach to RTL Verification -- Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development? -- Invited Tutorials -- Algorithms for Interface Synthesis -- A Tutorial on Satisfiability Modulo Theories -- A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java -- Verification of Hybrid Systems -- Session I: Compositionality -- SAT-Based Compositional Verification Using Lazy Learning -- Local Proofs for Global Safety Properties -- Session II: Verification Process -- Low-Level Library Analysis and Summarization -- Verification Across Intellectual Property Boundaries -- Session III: Timed Synthesis and Games -- On Synthesizing Controllers from Bounded-Response Properties -- An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games -- UPPAAL-Tiga: Time for Playing Games! -- The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems -- Session IV: Infinitive State Verification -- Systematic Acceleration in Regular Model Checking -- Parameterized Verification of Infinite-State Processes with Global Conditions -- Session V: Tool Environment -- CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes -- jMoped: A Test Environment for Java Programs -- Hector: Software Model Checking with Cooperating Analysis Plugins -- The Why/Krakatoa/Caduceus Platform for Deductive Program Verification -- Session VI: Shapes -- Shape Analysis for Composite Data Structures -- Array Abstractions from Proofs -- Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures -- Revamping TVLA: Making Parametric Shape Analysis Competitive -- Session VII: Concurrent Program Verification -- Fast and Accurate Static Data-Race Detection for Concurrent Programs -- Parametric and Sliced Causality -- Spade: Verification of Multithreaded Dynamic and Recursive Programs -- Session VIII: Reactive Designs -- Anzu: A Tool for Property Synthesis -- RAT: A Tool for the Formal Analysis of Requirements -- Session IX: Parallelisation -- Parallelising Symbolic State-Space Generators -- I/O Efficient Accepting Cycle Detection -- Session X: Constraints and Decisions -- C32SAT: Checking C Expressions -- CVC3 -- BAT: The Bit-Level Analysis Tool -- LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals -- Session XI: Probabilistic Verification -- Three-Valued Abstraction for Continuous-Time Markov Chains -- Magnifying-Lens Abstraction for Markov Decision Processes -- Underapproximation for Model-Checking Based on Random Cryptographic Constructions -- Session XII: Abstraction -- Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra -- Structural Abstraction of Software Verification Conditions -- An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software -- Adaptive Symmetry Reduction -- Session XIII: Assume-Guarantee Reasoning -- From Liveness to Promptness -- Automated Assumption Generation for Compositional Verification -- Session XIV: Hybrid Systems -- Abstraction and Counterexample-Guided Construction of ?-Automata for Model Checking of Step-Discrete Linear Hybrid Models -- Test Coverage for Continuous and Hybrid Systems -- Hybrid Systems: From Verification to Falsification -- Session XV: Program Analysis -- Comparison Under Abstraction for Verifying Linearizability -- Leaping Loops in the Presence of Abstraction -- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis -- Session XVI: SAT and Decision Procedures -- A Decision Procedure for Bit-Vectors and Arrays -- Boolean Abstraction for Temporal Logic Satisfiability -- A Lazy and Layered SMT( ) Solver for Hard Industrial Verification Problems. |
Record Nr. | UNINA-9910484352003321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Formal Techniques in Real-Time and Fault-Tolerant Systems [[electronic resource] ] : 7th International Symposium, FTRTFT 2002, Co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 9-12, 2002. Proceedings / / edited by Werner Damm, Ernst-Rüdiger Olderog |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (X, 462 p.) |
Disciplina | 004/.33 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Programming languages (Electronic computers)
Software engineering Architecture, Computer Computer logic Microprocessors Special purpose computers Programming Languages, Compilers, Interpreters Software Engineering/Programming and Operating Systems Computer System Implementation Logics and Meanings of Programs Processor Architectures Special Purpose and Application-Based Systems |
ISBN | 3-540-45739-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Tutorials -- UppaaL Implementation Secrets -- Software Hazard and Safety Analysis -- Invited Papers -- Real-Time Operating Systems: Problems and Novel Solutions -- Real-Time UML -- Eager Class Initialization for Java -- Applications of Formal Methods in Biology -- An Overview of Formal Verification for the Time-Triggered Architecture -- Scheduler Modeling Based on the Controller Synthesis Paradigm -- Synthesis and Scheduling -- Component-Based Synthesis of Dependable Embedded Software -- From the Specification to the Scheduling of Time-Dependent Systems -- On Control with Bounded Computational Resources -- Timed Automata I -- Decidability of Safety Properties of Timed Multiset Rewriting -- Extending Timed Automaton and Real-Time Logic to Many-Valued Reasoning -- Fault Diagnosis for Timed Automata -- Bounded Model Checking -- Verification of Timed Automata via Satisfiability Checking -- Take It NP-Easy: Bounded Model Construction for Duration Calculus -- Towards Bounded Model Checking for the Universal Fragment of TCTL -- Verification and Conformance Testing -- A Typed Interrupt Calculus -- Parametric Verification of a Group Membership Algorithm -- A Method for Testing the Conformance of Real Time Systems -- UML Models and Model Checking -- A Probabilistic Extension of UML Statecharts -- Eliminating Queues from RT UML Model Representations -- Model Checking Timed UML State Machines and Collaborations -- Timed Automata II -- Partial Order Path Technique for Checking Parallel Timed Automata -- Constructing Test Automata from Graphical Real-Time Requirements. |
Record Nr. | UNISA-996465522303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Techniques in Real-Time and Fault-Tolerant Systems : 7th International Symposium, FTRTFT 2002, Co-sponsored by IFIP WG 2.2, Oldenburg, Germany, September 9-12, 2002. Proceedings / / edited by Werner Damm, Ernst-Rüdiger Olderog |
Edizione | [1st ed. 2002.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 |
Descrizione fisica | 1 online resource (X, 462 p.) |
Disciplina | 004/.33 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Programming languages (Electronic computers)
Software engineering Architecture, Computer Computer logic Microprocessors Special purpose computers Programming Languages, Compilers, Interpreters Software Engineering/Programming and Operating Systems Computer System Implementation Logics and Meanings of Programs Processor Architectures Special Purpose and Application-Based Systems |
ISBN | 3-540-45739-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Tutorials -- UppaaL Implementation Secrets -- Software Hazard and Safety Analysis -- Invited Papers -- Real-Time Operating Systems: Problems and Novel Solutions -- Real-Time UML -- Eager Class Initialization for Java -- Applications of Formal Methods in Biology -- An Overview of Formal Verification for the Time-Triggered Architecture -- Scheduler Modeling Based on the Controller Synthesis Paradigm -- Synthesis and Scheduling -- Component-Based Synthesis of Dependable Embedded Software -- From the Specification to the Scheduling of Time-Dependent Systems -- On Control with Bounded Computational Resources -- Timed Automata I -- Decidability of Safety Properties of Timed Multiset Rewriting -- Extending Timed Automaton and Real-Time Logic to Many-Valued Reasoning -- Fault Diagnosis for Timed Automata -- Bounded Model Checking -- Verification of Timed Automata via Satisfiability Checking -- Take It NP-Easy: Bounded Model Construction for Duration Calculus -- Towards Bounded Model Checking for the Universal Fragment of TCTL -- Verification and Conformance Testing -- A Typed Interrupt Calculus -- Parametric Verification of a Group Membership Algorithm -- A Method for Testing the Conformance of Real Time Systems -- UML Models and Model Checking -- A Probabilistic Extension of UML Statecharts -- Eliminating Queues from RT UML Model Representations -- Model Checking Timed UML State Machines and Collaborations -- Timed Automata II -- Partial Order Path Technique for Checking Parallel Timed Automata -- Constructing Test Automata from Graphical Real-Time Requirements. |
Record Nr. | UNINA-9910143892503321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2002 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Integration of Software Specification Techniques for Applications in Engineering [[electronic resource] ] : Priority Program SoftSpez of the German Research Foundation (DFG) Final Report / / edited by Hartmut Ehrig, Werner Damm, Jörg Desel, Martin Große-Rhode, Wolfgang Reif, Eckehard Schnieder, Engelbert Westkämper |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (X, 630 p. 126 illus.) |
Disciplina | 005.10943 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
ISBN |
1-280-30792-7
9786610307920 3-540-27863-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Integration of Software Specification Techniques for Applications in Engineering: Introduction and Overview of Results -- Integration of Software Specification Techniques for Applications in Engineering: Introduction and Overview of Results -- I: Reference Case Study Production Automation -- Basic Principles for Software Specification -- Challenges of Next Generation Manufacturing Systems -- Development of Hierarchical Broadcasting Software Architectures Using UML 2.0 -- An Engineer’s Workstation to Support Integrated Development of Flexible Production Control Systems -- A Formal Component Concept for the Specification of Industrial Control Systems -- II: Reference Case Study Traffic Control Systems -- Specification Methodology, Case Studies, and Experiments – An Introduction to the Subject Area of Traffic Control Systems -- Reference Case Study “Traffic Control Systems” for Comparison and Validation of Formal Specifications Using a Railway Model Demonstrator -- Precise Definition of the Single-Track Level Crossing in Radio-Based Operation in UML Notation and Specification of Safety Requirements -- Executable HybridUML and Its Application to Train Control Systems -- The Use of UML for Development of a Railway Interlocking System -- III: Petri Nets and Related Approaches in Engineering -- Process Description Languages and Methods: Introduction to the Chapter Petri Nets and Related Approaches in Engineering -- Specification and Formal Verification of Temporal Properties of Production Automation Systems -- STOP – Specification Technique of Operational Processes -- Specification and Validation of an Edge Router Discovery Protocol for Mobile Ad Hoc Networks -- A Guide to Modelling and Control with Modules of Signal Nets -- Conceptual Design of an Engineering Model for Product and Plant Automation -- IV: Charts -- to Subject Area “Charts” -- The Rhapsody Semantics of Statecharts (or, On the Executable Core of the UML) -- Interactive Verification of Statecharts -- Live Sequence Charts -- A Unifying Semantics for Sequential Function Charts -- V: Verification -- to Subject Area “Verification” -- “UML–ising” Formal Techniques -- Model Based Formal Verification of Distributed Production Control Systems -- Combining Formal Methods and Safety Analysis – The ForMoSA Approach -- Formal Verification of LSCs in the Development Process -- Verification of PLC Programs Given as Sequential Function Charts -- Modeling and Formal Verification of Production Automation Systems -- VI: Integration Modeling -- On Model Integration and Integration Modelling -- On the Integration of Modular Heterogeneous Specifications -- Semantical Integration of Object-Oriented Viewpoint Specification Techniques. |
Record Nr. | UNISA-996465653003316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Integration of Software Specification Techniques for Applications in Engineering : Priority Program SoftSpez of the German Research Foundation (DFG) Final Report / / edited by Hartmut Ehrig, Werner Damm, Jörg Desel, Martin Große-Rhode, Wolfgang Reif, Eckehard Schnieder, Engelbert Westkämper |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (X, 630 p. 126 illus.) |
Disciplina | 005.10943 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
ISBN |
1-280-30792-7
9786610307920 3-540-27863-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Integration of Software Specification Techniques for Applications in Engineering: Introduction and Overview of Results -- Integration of Software Specification Techniques for Applications in Engineering: Introduction and Overview of Results -- I: Reference Case Study Production Automation -- Basic Principles for Software Specification -- Challenges of Next Generation Manufacturing Systems -- Development of Hierarchical Broadcasting Software Architectures Using UML 2.0 -- An Engineer’s Workstation to Support Integrated Development of Flexible Production Control Systems -- A Formal Component Concept for the Specification of Industrial Control Systems -- II: Reference Case Study Traffic Control Systems -- Specification Methodology, Case Studies, and Experiments – An Introduction to the Subject Area of Traffic Control Systems -- Reference Case Study “Traffic Control Systems” for Comparison and Validation of Formal Specifications Using a Railway Model Demonstrator -- Precise Definition of the Single-Track Level Crossing in Radio-Based Operation in UML Notation and Specification of Safety Requirements -- Executable HybridUML and Its Application to Train Control Systems -- The Use of UML for Development of a Railway Interlocking System -- III: Petri Nets and Related Approaches in Engineering -- Process Description Languages and Methods: Introduction to the Chapter Petri Nets and Related Approaches in Engineering -- Specification and Formal Verification of Temporal Properties of Production Automation Systems -- STOP – Specification Technique of Operational Processes -- Specification and Validation of an Edge Router Discovery Protocol for Mobile Ad Hoc Networks -- A Guide to Modelling and Control with Modules of Signal Nets -- Conceptual Design of an Engineering Model for Product and Plant Automation -- IV: Charts -- to Subject Area “Charts” -- The Rhapsody Semantics of Statecharts (or, On the Executable Core of the UML) -- Interactive Verification of Statecharts -- Live Sequence Charts -- A Unifying Semantics for Sequential Function Charts -- V: Verification -- to Subject Area “Verification” -- “UML–ising” Formal Techniques -- Model Based Formal Verification of Distributed Production Control Systems -- Combining Formal Methods and Safety Analysis – The ForMoSA Approach -- Formal Verification of LSCs in the Development Process -- Verification of PLC Programs Given as Sequential Function Charts -- Modeling and Formal Verification of Production Automation Systems -- VI: Integration Modeling -- On Model Integration and Integration Modelling -- On the Integration of Modular Heterogeneous Specifications -- Semantical Integration of Object-Oriented Viewpoint Specification Techniques. |
Record Nr. | UNINA-9910144347603321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|