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.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.13994 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer International Publishing AG,, 2023. ©2023. |
Year of Publication: | 2023 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (615 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5007240887 |
---|---|
ctrlnum |
(MiAaPQ)5007240887 (Au-PeEL)EBL7240887 (OCoLC)1377209783 |
collection |
bib_alma |
record_format |
marc |
spelling |
Sankaranarayanan, Sriram. 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. 1st ed. Cham : Springer International Publishing AG, 2023. ©2023. 1 online resource (615 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.13994 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. Description based on publisher supplied metadata and other sources. Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. Electronic books. Sharygina, Natasha. Print version: Sankaranarayanan, Sriram Tools and Algorithms for the Construction and Analysis of Systems Cham : Springer International Publishing AG,c2023 9783031308192 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=7240887 Click to View |
language |
English |
format |
eBook |
author |
Sankaranarayanan, Sriram. |
spellingShingle |
Sankaranarayanan, Sriram. 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. Lecture Notes in Computer Science Series ; 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. |
author_facet |
Sankaranarayanan, Sriram. Sharygina, Natasha. |
author_variant |
s s ss |
author2 |
Sharygina, Natasha. |
author2_variant |
n s ns |
author2_role |
TeilnehmendeR |
author_sort |
Sankaranarayanan, Sriram. |
title |
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. |
title_sub |
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. |
title_full |
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. |
title_fullStr |
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. |
title_full_unstemmed |
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. |
title_auth |
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. |
title_new |
Tools and Algorithms for the Construction and Analysis of Systems : |
title_sort |
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. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2023 |
physical |
1 online resource (615 pages) |
edition |
1st ed. |
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. |
isbn |
9783031308208 9783031308192 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA75 |
callnumber-sort |
QA 275.5 276.95 |
genre |
Electronic books. |
genre_facet |
Electronic books. |
url |
https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=7240887 |
illustrated |
Not Illustrated |
oclc_num |
1377209783 |
work_keys_str_mv |
AT sankaranarayanansriram toolsandalgorithmsfortheconstructionandanalysisofsystems29thinternationalconferencetacas2023heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2023parisfranceapril22272023proceedingspartii AT sharyginanatasha toolsandalgorithmsfortheconstructionandanalysisofsystems29thinternationalconferencetacas2023heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2023parisfranceapril22272023proceedingspartii |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5007240887 (Au-PeEL)EBL7240887 (OCoLC)1377209783 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.13994 |
is_hierarchy_title |
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. |
container_title |
Lecture Notes in Computer Science Series ; v.13994 |
author2_original_writing_str_mv |
noLinkedField |
marc_error |
Info : MARC8 translation shorter than ISO-8859-1, choosing MARC8. --- [ 856 : z ] |
_version_ |
1792331066027016192 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11369nam a22004693i 4500</leader><controlfield tag="001">5007240887</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073848.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2023 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783031308208</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783031308192</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5007240887</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL7240887</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1377209783</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA75.5-76.95</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Sankaranarayanan, Sriram.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Tools and Algorithms for the Construction and Analysis of Systems :</subfield><subfield code="b">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.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing AG,</subfield><subfield code="c">2023.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2023.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (615 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.13994</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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).</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">1.1 Using fewer universal variables.</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="590" ind1=" " ind2=" "><subfield code="a">Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. </subfield></datafield><datafield tag="655" ind1=" " ind2="4"><subfield code="a">Electronic books.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Sharygina, Natasha.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Sankaranarayanan, Sriram</subfield><subfield code="t">Tools and Algorithms for the Construction and Analysis of Systems</subfield><subfield code="d">Cham : Springer International Publishing AG,c2023</subfield><subfield code="z">9783031308192</subfield></datafield><datafield tag="797" ind1="2" ind2=" "><subfield code="a">ProQuest (Firm)</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=7240887</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |