Cover Image

Tools and Algorithms for the Construction and Analysis of Systems : 29th International Conference, TACAS 2023, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II.

Bibliographic Details
Main Author: Sankaranarayanan, Sriram.
Other Authors: Sharygina, Natasha.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2023.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
Table of Contents:
  • Intro
  • ETAPS Foreword
  • Preface
  • Organization
  • Contents - Part II
  • Contents - Part I
  • Tool Demos
  • EVA: a Tool for the Compositional Verification of AUTOSAR Models
  • 1 Introduction
  • 2 A Case Study for Verification in AUTOSAR
  • 3 EVA Verification Workflow
  • 4 Experimental Evaluation
  • 5 Data Availability Statement
  • References
  • WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification
  • 1 Introduction
  • 2 WASIM Functionalities
  • 2.1 Input Processing.
  • 2.2 Representing Simulation States using SMT formulas.
  • 2.3 Symbolic Simulation.
  • 2.4 Expression Simpilification
  • 2.5 Abstraction Refinement.
  • 3 User Interface
  • 3.1 Simulation Process Control.
  • 3.2 Customizable Abstraction/Refinement Function.
  • 3.3 Symbolic State Extraction and Manipulation.
  • 4 Case Studies
  • 5 Related Works
  • 6 Conclusions
  • Data Availability Statement
  • References
  • Multiparty Session Typing in Java, Deductively
  • 1 Introduction
  • 2 Usage: BGJ in a Nutshell
  • 3 Implementation
  • 4 Preliminary Evaluation
  • 5 Conclusion
  • Data Availability Statement
  • References
  • PyLTA: A Verification Tool for Parameterized Distributed Algorithms
  • 1 Introduction
  • 2 Modeling Distributed Algorithms
  • 3 Input Format and Usage
  • 4 Tool Overview and Usage
  • 5 Conclusion
  • References
  • FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
  • 1 Introduction
  • 2 Word-Level Model Checking and Btor2 Format
  • 3 The FuzzBtor2 Tool
  • 3.1 Usage
  • 3.2 Architecture
  • 4 Experimental Evaluation
  • 5 Conclusion
  • References
  • Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit
  • 1 Introduction
  • 2 Supervisory Controller Synthesis
  • 3 Synthesis-based Engineering Process
  • 4 Technical Improvements
  • 5 Case Studies and Applications
  • 6 Conclusions.
  • 7 Data-Availability Statement
  • References
  • Combinatorial Optimization/Theorem Proving
  • New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
  • 1 Introduction
  • 2 Preliminaries
  • 3 Core-Guided Algorithm
  • 3.1 Algorithm Description
  • 3.2 Algorithm Properties
  • 4 Hitting Set-based Algorithm
  • 4.1 Algorithm Description
  • 4.2 Algorithm Properties
  • 5 Experimental Results
  • 5.1 Algorithms and Implementation
  • 5.2 Experimental Setup and Benchmark Sets
  • 5.3 Results and Analysis
  • 6 Conclusions
  • Acknowledgements
  • References
  • Verified Reductions for Optimization
  • 1 Introduction
  • 2 Optimization Problems and Reductions
  • 3 Reduction to Conic Form
  • 4 Verifying the Reduction
  • 5 Adding Atoms
  • 6 User-defined Reductions
  • 7 Connecting Lean to a Conic Optimization Solver
  • 8 Related Work
  • 9 Conclusions
  • References
  • Specifying and Verifying Higher-order Rust Iterators
  • 1 Introduction
  • 1.1 Contributions
  • 2 Specifications in Rust Programs
  • 3 Reasoning on Iteration
  • 3.1 Specifying Iterators
  • 3.2 Structural Invariant of for Loops
  • 4 Examples of Specifications of Simple Iterators
  • 4.1 The Range Iterator
  • 4.2 IterMut: Mutating Iteration Over a Vector
  • 4.3 Iterator Adapters
  • 5 Closures in Rust
  • 6 A Higher-order Iterator Adapter: Map
  • 7 Evaluation
  • 8 Related and Future Work
  • Data availability
  • References
  • Extending a High-Performance Prover to Higher-Order Logic
  • 1 Introduction
  • 2 Logic
  • 3 Terms
  • 4 Unification, Matching, and Term Indexing
  • 5 Preprocessing, Calculus, and Extensions
  • 6 Evaluation
  • 7 Discussion and Related Work
  • 8 Conclusion
  • References
  • Tools (Regular Papers)
  • The WhyRel Prototype for Modular Relational Verification of Pointer Programs
  • 1 Introduction
  • 2 A tour of WhyRel
  • 3 Patterns of alignment
  • 4 Encoding and design.
  • 5 Evaluation
  • 6 Related work
  • 7 Conclusion
  • Acknowledgments
  • References
  • Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator
  • 1 Introduction
  • 1.1 Our Motivations and Contributions
  • 1.2 Example
  • 2 Related Work
  • 2.1 Compiling Hardware to Software
  • 2.2 Compiling Hardware to Intermediate Representation
  • 3 Background
  • 3.1 The Btor2 Language
  • 3.2 Sequential Circuits and Hardware Model Checking
  • 3.3 Software Model Checking
  • 4 Translating Btor2 to C
  • 4.1 Simulating Sequential Circuits with C Programs
  • 4.2 Variable Naming
  • 4.3 Expressing Btor2 Sorts in C
  • 4.4 Implementing Btor2 Operators in C
  • 4.5 Applying Modulo Operations Lazily
  • 4.6 Discussion
  • 5 Evaluation
  • 5.1 Benchmark Set
  • 5.2 State-of-the-Art Hardware and Software Analysis
  • 5.3 Experimental Setup
  • 5.4 Results
  • 5.5 Discussion
  • 6 Conclusion
  • Acknowledgements.
  • References
  • CoPTIC: Constraint Programming Translated Into C
  • 1 Introduction
  • 2 The Guess-and-Check Paradigm
  • 2.1 Constraint Satisfaction: Magic Square
  • 2.2 CoPTIC Architecture
  • 2.3 Planning: Knight's Tour
  • 2.4 Enumeration: Integer Quadratics
  • 2.5 Optimisation: Golomb Rulers
  • 3 Practical Considerations
  • 3.1 Debugging Constraint Models
  • 3.2 Performance
  • 4 Evaluation on CSPLib Problems
  • 5 Related Work
  • 6 Conclusion
  • Data Availability Statement
  • References
  • Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability
  • 1 Introduction
  • 2 Preliminaries
  • 3 Realizability algorithm
  • 3.1 Boolean states
  • 3.2 Actions
  • 3.3 Su cient inputs
  • 3.4 Algorithm
  • 4 The many options at every line
  • 4.1 Preprocessing of the automaton (line 1)
  • 4.2 Boolean states (line 2)
  • 4.3 Vectors and downsets (line 3)
  • 4.4 Selecting su cient inputs (line 5)
  • 4.5 Precomputing actions (line 6).
  • 4.6 Main loop: Picking input-actions (line 8)
  • 4.7 When are we done?
  • 5 Checking unrealizability of LTL specfications
  • 6 Benchmarks
  • 6.1 Protocol
  • 6.2 Results
  • 7 Conclusion
  • Acknowledgements.
  • References
  • Synthesis
  • Computing Adequately Permissive Assumptions for Synthesis
  • 1 Introduction
  • 2 Preliminaries
  • 3 Adequately Permissive Assumptions for Synthesis
  • 4 Computing Adequately Permissive Assumptions (APA)
  • 4.1 Preliminaries
  • 4.2 Safety Games
  • 4.3 Live Group Assumptions for Büchi Games
  • 4.4 Co-Liveness Assumptions in Co-Büchi Games
  • 4.5 APA Assumptions for Parity Games
  • 5 Experimental Evaluation
  • 5.1 Performance Evaluation
  • 5.2 2-Client Arbiter Example
  • References
  • Verification-guided Programmatic Controller Synthesis
  • 1 Introduction
  • 2 Problem Setup
  • 3 Programmatic Controllers
  • 4 Proof Space Optimization
  • 4.1 Controller Verification
  • 4.2 Correctness Property Loss in the Proof Space
  • 4.3 Controller Synthesis
  • 5 Experimental Results
  • 6 Related Work
  • 7 Conclusion
  • Acknowledgments
  • References
  • Taming Large Bounds in Synthesis from Bounded-Liveness Specifications
  • 1 Introduction
  • 2 Preliminaries
  • 3 SafeLTLB Synthesis with Countdown-Timer Games
  • 4 Countdown-Timer Game Construction
  • 4.1 Construction of a Countdown-Timer Game from SafeLTLB
  • 5 Solving Countdown-Timer Games
  • 6 Evaluation
  • 7 Conclusion
  • References
  • Lockstep Composition for Unbalanced Loops
  • 1 Introduction
  • 2 Related Work
  • 3 Illustration on Example
  • 4 Preliminaries
  • 4.1 Constrained Horn Clauses
  • 4.2 Relational Verification
  • 5 Equivalence Checking for Unbalanced Loops
  • 5.1 Input Limitations and Auxiliary Definitions
  • 5.2 Equivalence Checking by Decomposition
  • 5.3 Refinement
  • 6 Aligning Unbalanced Loops
  • 6.1 Finding the Number of Iterations
  • 6.2 Identifying Unrolling Depths.
  • 6.3 Rearrangement of the Source Projection
  • 7 Evaluation
  • 8 Conclusion
  • References
  • Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification
  • 1 Introduction
  • 2 The Mercury Parameterized Synthesis Problem
  • 2.1 Review: Mercury Systems
  • 2.2 Mercury Process Sketch
  • 2.3 Problem Definition
  • 3 Constraint-Based Synthesis for Mercury Systems
  • 4 Counterexample Extraction
  • 5 Implementation and Evaluation
  • 5.1 Implementation
  • 5.2 Evaluation
  • 6 Related Work
  • References
  • LTL Reactive Synthesis with a Few Hints
  • 1 Introduction
  • 2 Preliminaries on the reactive synthesis problem
  • 3 Synthesis from safety specifications and examples
  • 4 Synthesis from w-regular specifications and examples
  • 5 Implementation and Case study
  • 6 Conclusion
  • References
  • Timed Automata Verification and Synthesis via Finite Automata Learning
  • 1 Introduction
  • 2 Compositional Model Checking
  • 2.1 Preliminaries
  • 2.2 Learning-Based Compositional Model Checking Algorithm
  • 2.3 Experiments
  • 3 Compositional Controller Synthesis
  • 3.1 Preliminaries
  • 3.2 One-Sided Abstraction
  • 3.3 Learning-Based Compositional Controller Synthesis Algorithm
  • 3.4 Experiments
  • 4 Conclusion
  • References
  • Graphs/Probabilistic Systems
  • A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
  • 1 Introduction
  • 1.1 Our Contributions
  • 2 Preliminaries
  • 3 The Chain Algorithm
  • 3.1 Algorithm
  • 3.2 Correctness
  • 3.3 Complexity Analysis
  • 4 Extension to Colored Graphs
  • 4.1 Edge-Colored Graphs
  • 4.2 The ColoredChain Algorithm
  • 5 Experiments
  • 5.1 Experiments on Synthetic Benchmarks
  • 5.2 Experiments on Uncolored Graphs
  • 5.3 Experiments on Colored Graphs
  • 6 Conclusion
  • Acknowledgements.
  • References
  • Transforming Quantified Boolean Formulas Using Biclique Covers
  • 1 Introduction.
  • 1.1 Using fewer universal variables.

Similar Items