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.
Concise Guide to Software Verification : From Model Checking to Annotation Checking / / Marieke Huisman and Anton Wijs
| Concise Guide to Software Verification : From Model Checking to Annotation Checking / / Marieke Huisman and Anton Wijs |
| Autore | Huisman Marieke |
| Edizione | [First edition.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] |
| Descrizione fisica | 1 online resource (IX, 248 p. 146 illus., 127 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Texts in Computer Science Series |
| Soggetto topico | Computer software - Verification |
| ISBN | 3-031-30167-6 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1. Introduction -- 2. Background on First-Order Logic and Set Theory -- 3. System Modelling -- 4. Crash Course on Temporal Logic and its Verification -- 5. Software Analysis -- 6. Crash Course on Design by Contract Specifications -- 7. Run-time checking of Design by Contract Specifications -- 8. Static Checking of Design by Contract Specification -- 9. Abstract Specifications. |
| Record Nr. | UNINA-9910735783103321 |
Huisman Marieke
|
||
| Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Concise Guide to Software Verification : From Model Checking to Annotation Checking / / Marieke Huisman and Anton Wijs
| Concise Guide to Software Verification : From Model Checking to Annotation Checking / / Marieke Huisman and Anton Wijs |
| Autore | Huisman Marieke |
| Edizione | [First edition.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] |
| Descrizione fisica | 1 online resource (IX, 248 p. 146 illus., 127 illus. in color.) |
| Disciplina | 005.14 |
| Collana | Texts in Computer Science Series |
| Soggetto topico | Computer software - Verification |
| ISBN | 3-031-30167-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1. Introduction -- 2. Background on First-Order Logic and Set Theory -- 3. System Modelling -- 4. Crash Course on Temporal Logic and its Verification -- 5. Software Analysis -- 6. Crash Course on Design by Contract Specifications -- 7. Run-time checking of Design by Contract Specifications -- 8. Static Checking of Design by Contract Specification -- 9. Abstract Specifications. |
| Record Nr. | UNISA-996547964503316 |
|
Huisman Marieke
|
||
| Cham, Switzerland : , : Springer Nature Switzerland AG, , [2023] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal aspects of component software : 17th international conference, FACS 2021, virtual event, October 28-29, 2021 : proceedings / / edited by Gwen Salaün and Anton Wijs
| Formal aspects of component software : 17th international conference, FACS 2021, virtual event, October 28-29, 2021 : proceedings / / edited by Gwen Salaün and Anton Wijs |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (182 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Formal methods (Computer science) Component software |
| ISBN | 3-030-90636-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Parametric and Interval Model Checking: Recent Advances and Applications (Abstract of Invited Paper) -- Contents -- Invited Paper -- Learning Assumptions for Verifying Cryptographic Protocols Compositionally -- 1 Introduction -- 2 Background -- 2.1 Labeled Transition Systems -- 2.2 Assumption Learning and Alphabet Refinement -- 3 An Overview of Taglierino -- 4 The Attacker Model and Its Correctness -- 5 Protocol Analysis -- 5.1 Evaluation Setup -- 5.2 Needham-Schroeder-Lowe -- 5.3 Denning-Sacco -- 5.4 Woo-Lam -- 5.5 Kerberos -- 5.6 Performance Evaluation Results -- 6 Related Work -- 7 Conclusion -- References -- Modelling and Composition -- Component-Based Approach Combining UML and BIP for Rigorous System Design -- 1 Introduction -- 2 System Modeling with UML -- 2.1 Case Study -- 2.2 Architecture Model -- 2.3 Behavior Models -- 3 From UML to BIP -- 4 System Simulation and Verification -- 5 Related Work -- 6 Conclusion -- References -- Composable Partial Multiparty Session Types -- 1 Introduction -- 2 A Calculus for Processes over Multiparty Sessions -- 3 Partial Multiparty Session Types -- 4 Type System -- 5 Merging Partial Session Types -- 5.1 Mapping Merging Functions over Session Types -- 5.2 Merging Communications and Session Types -- 6 Subject Reduction and Progress -- 7 Related Work -- 8 Conclusions -- References -- A Canonical Algebra of Open Transition Systems -- 1 Introduction -- 1.1 State from Feedback -- 1.2 The Algebra of Transition Systems -- 1.3 Stateful and Stateless Components -- 1.4 Canonicity and Our Original Contribution -- 1.5 Related Work -- 1.6 Synopsis -- 1.7 Conventions -- 2 Preliminaries: Categories with Feedback -- 2.1 Categories with Feedback -- 2.2 Traced Monoidal Categories -- 2.3 Delay and Feedback -- 2.4 St(), the Free Category with Feedback -- 2.5 Examples.
3 Span(Graph): An Algebra of Transition Systems -- 3.1 The Algebra of Span(Graph) -- 3.2 The Components of Span(Graph) -- 3.3 Span(Graph) as a Category with Feedback -- 3.4 Cospan(Graph) as a Category with Feedback -- 3.5 Syntactical Presentation of Cospan(FinGraph) -- 4 Conclusions and Further Work -- References -- Corinne, a Tool for Choreography Automata -- 1 Introduction -- 2 Choreography Automata -- 3 Corinne -- 4 Conclusion, Related Work, and Future Work -- References -- Verification -- Specification and Safety Verification of Parametric Hierarchical Distributed Systems -- 1 Introduction -- 2 Preliminaries -- 3 A Term Algebra of Behaviors -- 4 The Parametric Safety Problem -- 4.1 Encoding Invariants and Error Configurations -- 4.2 The Flow of a Behavioral Term -- 5 Experimental Evaluation -- 6 Related Work -- 7 Conclusions and Future Work -- References -- A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions -- 1 Introduction -- 2 Preliminaries -- 2.1 The PRAM Model -- 2.2 Strong Bisimulation -- 3 Relational Coarsest Partition Problem -- 3.1 The Sequential Algorithm -- 3.2 The PRAM Algorithm -- 3.3 Correctness -- 3.4 Complexity Analysis -- 4 Bisimulation Coarsest Refinement Problem -- 4.1 The PRAM Algorithm -- 4.2 Complexity and Correctness -- 5 Experimental Results -- 5.1 Experimental Comparison -- 6 Conclusion -- References -- Automated Generation of Initial Configurations for Testing Component Systems -- 1 Introduction -- 2 Background -- 3 Component-Based Model -- 4 Generation of Initial Configurations -- 4.1 Combinatorial Algorithm -- 4.2 Initial Configuration Sampling -- 4.3 Integration into the Online Test Generation Process -- 5 Experimentation -- 6 Related Work -- 7 Conclusion and Future Works -- References -- Monitoring Distributed Component-Based Systems -- 1 Introduction. 2 Preliminaries and Notations -- 3 Distributed CBS -- 3.1 Semantics -- 3.2 Traces -- 4 Efficient Construction of the Computation Lattice -- 4.1 Computation Lattice -- 4.2 Intermediate Operations -- 4.3 Algorithms for Constructing the Computation Lattice -- 5 Properties of the Constructed Lattice -- 5.1 Insensitivity to Communication Delay -- 5.2 Correctness of Lattice Construction -- 6 Related Work -- 7 Conclusions -- References -- Author Index. |
| Record Nr. | UNISA-996464409603316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Formal aspects of component software : 17th international conference, FACS 2021, virtual event, October 28-29, 2021 : proceedings / / edited by Gwen Salaün and Anton Wijs
| Formal aspects of component software : 17th international conference, FACS 2021, virtual event, October 28-29, 2021 : proceedings / / edited by Gwen Salaün and Anton Wijs |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (182 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Formal methods (Computer science) Component software |
| ISBN | 3-030-90636-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Parametric and Interval Model Checking: Recent Advances and Applications (Abstract of Invited Paper) -- Contents -- Invited Paper -- Learning Assumptions for Verifying Cryptographic Protocols Compositionally -- 1 Introduction -- 2 Background -- 2.1 Labeled Transition Systems -- 2.2 Assumption Learning and Alphabet Refinement -- 3 An Overview of Taglierino -- 4 The Attacker Model and Its Correctness -- 5 Protocol Analysis -- 5.1 Evaluation Setup -- 5.2 Needham-Schroeder-Lowe -- 5.3 Denning-Sacco -- 5.4 Woo-Lam -- 5.5 Kerberos -- 5.6 Performance Evaluation Results -- 6 Related Work -- 7 Conclusion -- References -- Modelling and Composition -- Component-Based Approach Combining UML and BIP for Rigorous System Design -- 1 Introduction -- 2 System Modeling with UML -- 2.1 Case Study -- 2.2 Architecture Model -- 2.3 Behavior Models -- 3 From UML to BIP -- 4 System Simulation and Verification -- 5 Related Work -- 6 Conclusion -- References -- Composable Partial Multiparty Session Types -- 1 Introduction -- 2 A Calculus for Processes over Multiparty Sessions -- 3 Partial Multiparty Session Types -- 4 Type System -- 5 Merging Partial Session Types -- 5.1 Mapping Merging Functions over Session Types -- 5.2 Merging Communications and Session Types -- 6 Subject Reduction and Progress -- 7 Related Work -- 8 Conclusions -- References -- A Canonical Algebra of Open Transition Systems -- 1 Introduction -- 1.1 State from Feedback -- 1.2 The Algebra of Transition Systems -- 1.3 Stateful and Stateless Components -- 1.4 Canonicity and Our Original Contribution -- 1.5 Related Work -- 1.6 Synopsis -- 1.7 Conventions -- 2 Preliminaries: Categories with Feedback -- 2.1 Categories with Feedback -- 2.2 Traced Monoidal Categories -- 2.3 Delay and Feedback -- 2.4 St(), the Free Category with Feedback -- 2.5 Examples.
3 Span(Graph): An Algebra of Transition Systems -- 3.1 The Algebra of Span(Graph) -- 3.2 The Components of Span(Graph) -- 3.3 Span(Graph) as a Category with Feedback -- 3.4 Cospan(Graph) as a Category with Feedback -- 3.5 Syntactical Presentation of Cospan(FinGraph) -- 4 Conclusions and Further Work -- References -- Corinne, a Tool for Choreography Automata -- 1 Introduction -- 2 Choreography Automata -- 3 Corinne -- 4 Conclusion, Related Work, and Future Work -- References -- Verification -- Specification and Safety Verification of Parametric Hierarchical Distributed Systems -- 1 Introduction -- 2 Preliminaries -- 3 A Term Algebra of Behaviors -- 4 The Parametric Safety Problem -- 4.1 Encoding Invariants and Error Configurations -- 4.2 The Flow of a Behavioral Term -- 5 Experimental Evaluation -- 6 Related Work -- 7 Conclusions and Future Work -- References -- A Linear Parallel Algorithm to Compute Bisimulation and Relational Coarsest Partitions -- 1 Introduction -- 2 Preliminaries -- 2.1 The PRAM Model -- 2.2 Strong Bisimulation -- 3 Relational Coarsest Partition Problem -- 3.1 The Sequential Algorithm -- 3.2 The PRAM Algorithm -- 3.3 Correctness -- 3.4 Complexity Analysis -- 4 Bisimulation Coarsest Refinement Problem -- 4.1 The PRAM Algorithm -- 4.2 Complexity and Correctness -- 5 Experimental Results -- 5.1 Experimental Comparison -- 6 Conclusion -- References -- Automated Generation of Initial Configurations for Testing Component Systems -- 1 Introduction -- 2 Background -- 3 Component-Based Model -- 4 Generation of Initial Configurations -- 4.1 Combinatorial Algorithm -- 4.2 Initial Configuration Sampling -- 4.3 Integration into the Online Test Generation Process -- 5 Experimentation -- 6 Related Work -- 7 Conclusion and Future Works -- References -- Monitoring Distributed Component-Based Systems -- 1 Introduction. 2 Preliminaries and Notations -- 3 Distributed CBS -- 3.1 Semantics -- 3.2 Traces -- 4 Efficient Construction of the Computation Lattice -- 4.1 Computation Lattice -- 4.2 Intermediate Operations -- 4.3 Algorithms for Constructing the Computation Lattice -- 5 Properties of the Constructed Lattice -- 5.1 Insensitivity to Communication Delay -- 5.2 Correctness of Lattice Construction -- 6 Related Work -- 7 Conclusions -- References -- Author Index. |
| Record Nr. | UNINA-9910508443803321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
iFM 2023 [[electronic resource] ] : 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings / / edited by Paula Herber, Anton Wijs
| iFM 2023 [[electronic resource] ] : 18th International Conference, iFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings / / edited by Paula Herber, Anton Wijs |
| Autore | Herber Paula |
| Edizione | [1st ed. 2024.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
| Descrizione fisica | 1 online resource (405 pages) |
| Disciplina | 005.1 |
| Altri autori (Persone) | WijsAnton |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Software Engineering |
| ISBN | 3-031-47705-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstract of Invited Talks -- Formal Signoff Flows -- Industrial Experience with a Verification-Aware Programming Language -- Contents -- Invited Presentations -- SMT: Something You Must Try -- 1 Introduction -- 2 Satisfiability Checking -- 2.1 SAT Solving -- 2.2 SMT Solving -- 3 Applications -- 3.1 A Toy Encoding Example -- 3.2 Planning with Optimization Modulo Theories -- 3.3 Reachability Analysis for Hybrid Systems with HyPro -- 3.4 Parameter Synthesis for Probabilistic Systems -- 4 Hybrid Petri Nets and Rate Adaption -- 4.1 Hybrid Petri Nets -- 4.2 Rate Adaption -- 4.3 Formulation as an SMT Problem -- 5 Some Final Remarks -- References -- Analysis and Verification -- Automated Sensitivity Analysis for Probabilistic Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Syntax and Semantics of Probabilistic Loops -- 2.2 C-finite Recurrences -- 2.3 Higher Moment Analysis Using Recurrences -- 3 Sensitivity Analysis -- 3.1 Sensitivity Analysis for Admissible Loops -- 3.2 Sensitivity Analysis for Non-admissible Loops -- 4 Experiments and Evaluation -- 5 Related Work -- 6 Conclusion -- References -- diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions -- 1 Introduction -- 2 Foundations of Difference Verification with Conditions -- 3 Dependency and Property Aware Difference Detection -- 4 Evaluation -- 4.1 Experimental Setup -- 4.2 Experimental Results -- 5 Related Work -- 6 Conclusion -- References -- CHC Model Validation with Proof Guarantees -- 1 Introduction -- 2 Background -- 2.1 Constrained Horn Clauses -- 2.2 Related Witness Validation Approaches -- 3 Validation of CHC Models -- 4 Implementation -- 5 Evaluation -- 5.1 Benchmarks and Tools -- 5.2 Model Validation Results -- 5.3 Proof Checking Results -- 6 Conclusions -- References.
VerifyThis: Memcached-A Practical Long-Term Challenge for the Integration of Formal Methods -- 1 Introduction -- 2 System Description -- 3 Challenge Goals -- 4 Participation, Time Schedule, Conclusion -- References -- Deductive Verification -- Towards Formal Verification of a TPM Software Stack -- 1 Introduction -- 2 Frama-C Verification Platform -- 3 The TPM Software Stack and the tpm2-tss Library -- 4 Dynamic Memory Allocation -- 5 Memory Management -- 6 Lemmas -- 7 Verification Results -- 8 Related Work -- 9 Conclusion and Future Work -- References -- Reasoning About Exceptional Behavior at the Level of Java Bytecode -- 1 Introduction -- 2 Motivating Example -- 3 Specifying and Verifying Exceptional Behavior -- 3.1 Specifying Exceptional Behavior -- 3.2 The Vimp Intermediate Representation -- 3.3 Modeling Exceptional Control Flow -- 3.4 Transformation Order and Boogie Code Generation -- 3.5 Implementation Details -- 4 Experiments -- 4.1 Programs -- 4.2 Results -- 5 Related Work -- 6 Conclusions -- References -- Analysis and Formal Specification of OpenJDK's BitSet -- 1 Introduction -- 2 The BitSet Class -- 3 Formal Specification -- 3.1 Class Invariant -- 3.2 The wordsToSeq() Model Method -- 3.3 The get(int,int) Method -- 4 Issues in BitSet -- 4.1 A Bug in get(int,int) Caused by a Negative length() -- 4.2 Bugs Caused by valueOf(...) Corrupting length() -- 4.3 Solution Directions -- 5 Towards Formal Verification of the BitSet Class -- 5.1 Background -- 5.2 Proof Sketch of get(int,int) -- 5.3 Required Extensions to KeY -- 6 Conclusion -- References -- Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation -- 1 Introduction -- 2 Design of the Specification Translator -- 3 Translating Annotations -- 3.1 OpenJML -- 3.2 Krakatoa -- 3.3 VerCors -- 4 Evaluation -- 4.1 Reuse of Specifications -- 4.2 Reuse of Tools. 5 Related Work -- 6 Conclusion -- References -- Hardware and Memory Verification -- Lifting the Reasoning Level in Generic Weak Memory Verification -- 1 Introduction -- 2 Program Syntax -- 3 Axiomatic Reasoning -- 3.1 Axioms -- 3.2 Reasoning Example on Axiom Level -- 4 Rules -- 5 Correctness Proof of WRC via Proof Rules -- 6 Related Work -- 7 Conclusion -- References -- Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction -- 1 Introduction -- 2 Background on Using Positive Equality to Formally Verify Pipelined Processors -- 3 Efficient Modeling of the RISC-V Architecture at a High Level of Abstraction -- 3.1 Abstraction of the Register File -- 3.2 Abstraction of the Decoding Logic -- 3.3 Abstraction of the CSR Memory Array -- 3.4 Non-Pipelined Specifications -- 3.5 Formal Verification of Liveness -- 3.6 Invariant Constraints Were Not Needed for the Correct Designs, but Were Proved for Debugging the 4-Stage Pipelined Processor -- 4 Modeling of Spatial Redundancy in Pipelined Processors at a High Level of Abstraction for Formal Verification of Safety -- 5 Results -- 6 Conclusion -- References -- Refinement and Separation: Modular Verification of Wandering Trees -- 1 Introduction -- 2 Wandering Trees -- 3 Structured Specifications of Algebraic Data Types -- 3.1 Algebraic Definitions -- 3.2 Modeling the Heap and Separation Logic -- 4 Modular Software Systems -- 5 Modularization -- 5.1 Specification of the Index -- 5.2 Index Refinement -- 5.3 Tree Refinement -- 5.4 Pointer Structures in the Heap and on Flash -- 6 Verification -- 6.1 Correctness of the Tree Component -- 6.2 Correctness of Wandering Trees -- 6.3 Correctness of Flash Representation -- 7 Conclusion -- References -- Verification and Learning. Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method -- 1 Introduction -- 2 Background -- 2.1 ProB and the B Method -- 2.2 Performance Fuzzing -- 2.3 Thompson Sampling -- 3 The BanditFuzz Algorithm -- 4 Adapting BanditFuzz for ProB -- 4.1 Fuzzing for Classical B Instead of SMT-LIB -- 4.2 Targeted Fuzzing and Mutating -- 4.3 Well-Defined ASTs -- 5 Running the Performance Fuzzer -- 5.1 Fuzzing only -- 5.2 Performance Fuzzing Between ProB's Backends -- 5.3 Performance Fuzzing Between ProB's Settings -- 5.4 Performance Fuzzing Between the SMT-LIB Translations -- 6 Related Work -- 7 Discussion -- 8 Conclusions -- References -- Reinforcement Learning Under Partial Observability Guided by Learned Environment Models -- 1 Introduction -- 2 Preliminaries -- 2.1 Models -- 2.2 Learning MDPs -- 3 QA-Learning: RL Assisted by Automata Learning -- 3.1 Overview -- 3.2 Extended State Space -- 3.3 Partially Observable Q-Learning -- 3.4 Convergence -- 3.5 Generalization and Limitations -- 4 Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Temporal Logics -- Mission-Time LTL (MLTL) Formula Validation via Regular Expressions -- 1 Introduction -- 2 Preliminaries: Mission-Time LTL and Bit String Computations -- 3 MLTL Regular Expressions -- 4 WEST Algorithm and Analysis -- 4.1 Proof of Correctness of WEST -- 4.2 Theoretical Complexity -- 4.3 Experimental Benchmarking -- 5 Correctness of WEST Tool Implementation -- 5.1 Intelligent Fuzzing -- 6 Regular Expression Simplification Theorem (REST) -- 6.1 Theoretical Analysis of REST -- 6.2 Experimental Benchmarking of REST -- 7 Using WEST: An Example -- 8 Closing Remarks -- 8.1 Future Work -- References -- Symbolic Model Checking of Relative Safety LTL Properties -- 1 Introduction -- 2 Motivating Examples -- 2.1 Bounded Response Example -- 2.2 Safety Contracts. 2.3 LTL G p vs. Invariant -- 3 Related Work -- 4 Notation and Preliminary Definitions -- 4.1 Notation for Sequences, Concatenation and Prefix -- 4.2 Safety and Relative Safety -- 4.3 LTL and Safety Fragments -- 4.4 Symbolic Transition System and Invariant Checking -- 4.5 Symbolic Techniques Reducing LTL Model Checking to Invariant Checking -- 5 Symbolic Compilation of Safety LTL -- 5.1 Symbolic Compilation of Full LTL -- 5.2 Symbolic Compilation of SafetyLTL -- 5.3 Symbolic Construction of Live Systems -- 6 Algorithm -- 6.1 Simple Algorithm Without Loops -- 6.2 CEGAR Loop Algorithm -- 6.3 Extending Algorithm with Lookahead -- 7 Experimental Evaluation -- 7.1 Benchmarks -- 7.2 Experimental Results and Analysis -- 8 Conclusions and Future Work -- References -- Extending PlusCal for Modeling Distributed Algorithms -- 1 Introduction -- 2 TLA+ and PlusCal -- 2.1 The Specification Language TLA+ -- 2.2 The Algorithmic Langage PlusCal -- 2.3 Translating PlusCal to TLA+ -- 3 Distributed PlusCal -- 3.1 Sub-processes -- 3.2 Communication Channels -- 4 Evaluation -- 4.1 Two Distributed Algorithms Expressed in Distributed PlusCal -- 4.2 Related Work -- 5 Conclusion -- References -- Autonomous Systems -- Formal Modelling and Analysis of a Self-Adaptive Robotic System -- 1 Introduction -- 2 Case Study: Pipeline Inspection by AUV -- 3 Modelling the AUV Case Study with ProFeat -- 3.1 The Feature Model -- 3.2 The Managed Subsystem -- 3.3 The Environment -- 3.4 The Managing Subsystem -- 4 Analysis -- 5 Related Work -- 6 Discussion and Future Work -- References -- CAN-verify: A Verification Tool For BDI Agents -- 1 Introduction -- 2 Can-Overview -- 3 CAN-verify Components and Features -- 4 Examples -- 5 Discussion and Conclusion -- References -- PhD Symposium Presentations -- Scalable and Precise Refinement Types for Imperative Languages -- 1 Introduction. 2 Combining Refinement Type Systems and Deductive Verification. |
| Record Nr. | UNISA-996565869703316 |
|
Herber Paula
|
||
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Integrated Formal Methods : 18th International Conference, IFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings / / edited by Paula Herber, Anton Wijs
| Integrated Formal Methods : 18th International Conference, IFM 2023, Leiden, The Netherlands, November 13–15, 2023, Proceedings / / edited by Paula Herber, Anton Wijs |
| Edizione | [1st ed. 2024.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
| Descrizione fisica | 1 online resource (405 pages) |
| Disciplina | 004.0151 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Software Engineering |
| ISBN | 3-031-47705-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstract of Invited Talks -- Formal Signoff Flows -- Industrial Experience with a Verification-Aware Programming Language -- Contents -- Invited Presentations -- SMT: Something You Must Try -- 1 Introduction -- 2 Satisfiability Checking -- 2.1 SAT Solving -- 2.2 SMT Solving -- 3 Applications -- 3.1 A Toy Encoding Example -- 3.2 Planning with Optimization Modulo Theories -- 3.3 Reachability Analysis for Hybrid Systems with HyPro -- 3.4 Parameter Synthesis for Probabilistic Systems -- 4 Hybrid Petri Nets and Rate Adaption -- 4.1 Hybrid Petri Nets -- 4.2 Rate Adaption -- 4.3 Formulation as an SMT Problem -- 5 Some Final Remarks -- References -- Analysis and Verification -- Automated Sensitivity Analysis for Probabilistic Loops -- 1 Introduction -- 2 Preliminaries -- 2.1 Syntax and Semantics of Probabilistic Loops -- 2.2 C-finite Recurrences -- 2.3 Higher Moment Analysis Using Recurrences -- 3 Sensitivity Analysis -- 3.1 Sensitivity Analysis for Admissible Loops -- 3.2 Sensitivity Analysis for Non-admissible Loops -- 4 Experiments and Evaluation -- 5 Related Work -- 6 Conclusion -- References -- diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions -- 1 Introduction -- 2 Foundations of Difference Verification with Conditions -- 3 Dependency and Property Aware Difference Detection -- 4 Evaluation -- 4.1 Experimental Setup -- 4.2 Experimental Results -- 5 Related Work -- 6 Conclusion -- References -- CHC Model Validation with Proof Guarantees -- 1 Introduction -- 2 Background -- 2.1 Constrained Horn Clauses -- 2.2 Related Witness Validation Approaches -- 3 Validation of CHC Models -- 4 Implementation -- 5 Evaluation -- 5.1 Benchmarks and Tools -- 5.2 Model Validation Results -- 5.3 Proof Checking Results -- 6 Conclusions -- References.
VerifyThis: Memcached-A Practical Long-Term Challenge for the Integration of Formal Methods -- 1 Introduction -- 2 System Description -- 3 Challenge Goals -- 4 Participation, Time Schedule, Conclusion -- References -- Deductive Verification -- Towards Formal Verification of a TPM Software Stack -- 1 Introduction -- 2 Frama-C Verification Platform -- 3 The TPM Software Stack and the tpm2-tss Library -- 4 Dynamic Memory Allocation -- 5 Memory Management -- 6 Lemmas -- 7 Verification Results -- 8 Related Work -- 9 Conclusion and Future Work -- References -- Reasoning About Exceptional Behavior at the Level of Java Bytecode -- 1 Introduction -- 2 Motivating Example -- 3 Specifying and Verifying Exceptional Behavior -- 3.1 Specifying Exceptional Behavior -- 3.2 The Vimp Intermediate Representation -- 3.3 Modeling Exceptional Control Flow -- 3.4 Transformation Order and Boogie Code Generation -- 3.5 Implementation Details -- 4 Experiments -- 4.1 Programs -- 4.2 Results -- 5 Related Work -- 6 Conclusions -- References -- Analysis and Formal Specification of OpenJDK's BitSet -- 1 Introduction -- 2 The BitSet Class -- 3 Formal Specification -- 3.1 Class Invariant -- 3.2 The wordsToSeq() Model Method -- 3.3 The get(int,int) Method -- 4 Issues in BitSet -- 4.1 A Bug in get(int,int) Caused by a Negative length() -- 4.2 Bugs Caused by valueOf(...) Corrupting length() -- 4.3 Solution Directions -- 5 Towards Formal Verification of the BitSet Class -- 5.1 Background -- 5.2 Proof Sketch of get(int,int) -- 5.3 Required Extensions to KeY -- 6 Conclusion -- References -- Joining Forces! Reusing Contracts for Deductive Verifiers Through Automatic Translation -- 1 Introduction -- 2 Design of the Specification Translator -- 3 Translating Annotations -- 3.1 OpenJML -- 3.2 Krakatoa -- 3.3 VerCors -- 4 Evaluation -- 4.1 Reuse of Specifications -- 4.2 Reuse of Tools. 5 Related Work -- 6 Conclusion -- References -- Hardware and Memory Verification -- Lifting the Reasoning Level in Generic Weak Memory Verification -- 1 Introduction -- 2 Program Syntax -- 3 Axiomatic Reasoning -- 3.1 Axioms -- 3.2 Reasoning Example on Axiom Level -- 4 Rules -- 5 Correctness Proof of WRC via Proof Rules -- 6 Related Work -- 7 Conclusion -- References -- Automatic Formal Verification of RISC-V Pipelined Microprocessors with Fault Tolerance by Spatial Redundancy at a High Level of Abstraction -- 1 Introduction -- 2 Background on Using Positive Equality to Formally Verify Pipelined Processors -- 3 Efficient Modeling of the RISC-V Architecture at a High Level of Abstraction -- 3.1 Abstraction of the Register File -- 3.2 Abstraction of the Decoding Logic -- 3.3 Abstraction of the CSR Memory Array -- 3.4 Non-Pipelined Specifications -- 3.5 Formal Verification of Liveness -- 3.6 Invariant Constraints Were Not Needed for the Correct Designs, but Were Proved for Debugging the 4-Stage Pipelined Processor -- 4 Modeling of Spatial Redundancy in Pipelined Processors at a High Level of Abstraction for Formal Verification of Safety -- 5 Results -- 6 Conclusion -- References -- Refinement and Separation: Modular Verification of Wandering Trees -- 1 Introduction -- 2 Wandering Trees -- 3 Structured Specifications of Algebraic Data Types -- 3.1 Algebraic Definitions -- 3.2 Modeling the Heap and Separation Logic -- 4 Modular Software Systems -- 5 Modularization -- 5.1 Specification of the Index -- 5.2 Index Refinement -- 5.3 Tree Refinement -- 5.4 Pointer Structures in the Heap and on Flash -- 6 Verification -- 6.1 Correctness of the Tree Component -- 6.2 Correctness of Wandering Trees -- 6.3 Correctness of Flash Representation -- 7 Conclusion -- References -- Verification and Learning. Performance Fuzzing with Reinforcement-Learning and Well-Defined Constraints for the B Method -- 1 Introduction -- 2 Background -- 2.1 ProB and the B Method -- 2.2 Performance Fuzzing -- 2.3 Thompson Sampling -- 3 The BanditFuzz Algorithm -- 4 Adapting BanditFuzz for ProB -- 4.1 Fuzzing for Classical B Instead of SMT-LIB -- 4.2 Targeted Fuzzing and Mutating -- 4.3 Well-Defined ASTs -- 5 Running the Performance Fuzzer -- 5.1 Fuzzing only -- 5.2 Performance Fuzzing Between ProB's Backends -- 5.3 Performance Fuzzing Between ProB's Settings -- 5.4 Performance Fuzzing Between the SMT-LIB Translations -- 6 Related Work -- 7 Discussion -- 8 Conclusions -- References -- Reinforcement Learning Under Partial Observability Guided by Learned Environment Models -- 1 Introduction -- 2 Preliminaries -- 2.1 Models -- 2.2 Learning MDPs -- 3 QA-Learning: RL Assisted by Automata Learning -- 3.1 Overview -- 3.2 Extended State Space -- 3.3 Partially Observable Q-Learning -- 3.4 Convergence -- 3.5 Generalization and Limitations -- 4 Evaluation -- 5 Related Work -- 6 Conclusion -- References -- Temporal Logics -- Mission-Time LTL (MLTL) Formula Validation via Regular Expressions -- 1 Introduction -- 2 Preliminaries: Mission-Time LTL and Bit String Computations -- 3 MLTL Regular Expressions -- 4 WEST Algorithm and Analysis -- 4.1 Proof of Correctness of WEST -- 4.2 Theoretical Complexity -- 4.3 Experimental Benchmarking -- 5 Correctness of WEST Tool Implementation -- 5.1 Intelligent Fuzzing -- 6 Regular Expression Simplification Theorem (REST) -- 6.1 Theoretical Analysis of REST -- 6.2 Experimental Benchmarking of REST -- 7 Using WEST: An Example -- 8 Closing Remarks -- 8.1 Future Work -- References -- Symbolic Model Checking of Relative Safety LTL Properties -- 1 Introduction -- 2 Motivating Examples -- 2.1 Bounded Response Example -- 2.2 Safety Contracts. 2.3 LTL G p vs. Invariant -- 3 Related Work -- 4 Notation and Preliminary Definitions -- 4.1 Notation for Sequences, Concatenation and Prefix -- 4.2 Safety and Relative Safety -- 4.3 LTL and Safety Fragments -- 4.4 Symbolic Transition System and Invariant Checking -- 4.5 Symbolic Techniques Reducing LTL Model Checking to Invariant Checking -- 5 Symbolic Compilation of Safety LTL -- 5.1 Symbolic Compilation of Full LTL -- 5.2 Symbolic Compilation of SafetyLTL -- 5.3 Symbolic Construction of Live Systems -- 6 Algorithm -- 6.1 Simple Algorithm Without Loops -- 6.2 CEGAR Loop Algorithm -- 6.3 Extending Algorithm with Lookahead -- 7 Experimental Evaluation -- 7.1 Benchmarks -- 7.2 Experimental Results and Analysis -- 8 Conclusions and Future Work -- References -- Extending PlusCal for Modeling Distributed Algorithms -- 1 Introduction -- 2 TLA+ and PlusCal -- 2.1 The Specification Language TLA+ -- 2.2 The Algorithmic Langage PlusCal -- 2.3 Translating PlusCal to TLA+ -- 3 Distributed PlusCal -- 3.1 Sub-processes -- 3.2 Communication Channels -- 4 Evaluation -- 4.1 Two Distributed Algorithms Expressed in Distributed PlusCal -- 4.2 Related Work -- 5 Conclusion -- References -- Autonomous Systems -- Formal Modelling and Analysis of a Self-Adaptive Robotic System -- 1 Introduction -- 2 Case Study: Pipeline Inspection by AUV -- 3 Modelling the AUV Case Study with ProFeat -- 3.1 The Feature Model -- 3.2 The Managed Subsystem -- 3.3 The Environment -- 3.4 The Managing Subsystem -- 4 Analysis -- 5 Related Work -- 6 Discussion and Future Work -- References -- CAN-verify: A Verification Tool For BDI Agents -- 1 Introduction -- 2 Can-Overview -- 3 CAN-verify Components and Features -- 4 Examples -- 5 Discussion and Conclusion -- References -- PhD Symposium Presentations -- Scalable and Precise Refinement Types for Imperative Languages -- 1 Introduction. 2 Combining Refinement Type Systems and Deductive Verification. |
| Record Nr. | UNINA-9910763597803321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Model Checking Software [[electronic resource] ] : 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings / / edited by Dragan Bošnački, Anton Wijs
| Model Checking Software [[electronic resource] ] : 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings / / edited by Dragan Bošnački, Anton Wijs |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVI, 245 p. 75 illus.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Machine theory Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-319-32582-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated Analysis of Asynchronously Communicating Systems -- Symbolic Game Semantics for Model Checking Program Families -- Compositional Semantics and Analysis of Hierarchical Block Diagrams -- Using SPIN for the Optimized Scheduling of Discrete Event Systems in Manufacturing -- River Basin Management with SPIN -- ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications -- Autonomous Agent Behaviour Modelled in PRISM -- Certication for -Calculus with Winning Strategies -- Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization -- Finite-Horizon Bisimulation Minimisation for Probabilistic Systems -- Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking -- smid: A Black-Box Program Driver -- On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators -- SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration -- A Tool Integrating Model Checking into a C Verification Toolset -- Fair Testing and Stubborn Sets. |
| Record Nr. | UNISA-996465717603316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Model Checking Software : 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings / / edited by Dragan Bošnački, Anton Wijs
| Model Checking Software : 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings / / edited by Dragan Bošnački, Anton Wijs |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 |
| Descrizione fisica | 1 online resource (XVI, 245 p. 75 illus.) |
| Disciplina | 005.14 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Compilers (Computer programs) Computer science Machine theory Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN | 3-319-32582-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated Analysis of Asynchronously Communicating Systems -- Symbolic Game Semantics for Model Checking Program Families -- Compositional Semantics and Analysis of Hierarchical Block Diagrams -- Using SPIN for the Optimized Scheduling of Discrete Event Systems in Manufacturing -- River Basin Management with SPIN -- ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications -- Autonomous Agent Behaviour Modelled in PRISM -- Certication for -Calculus with Winning Strategies -- Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization -- Finite-Horizon Bisimulation Minimisation for Probabilistic Systems -- Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking -- smid: A Black-Box Program Driver -- On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators -- SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration -- A Tool Integrating Model Checking into a C Verification Toolset -- Fair Testing and Stubborn Sets. |
| Record Nr. | UNINA-9910483225203321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||