Tools and Algorithms for the Construction and Analysis of Systems : : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.12652 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer International Publishing AG,, 2021. ©2021. |
Year of Publication: | 2021 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (476 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5006524978 |
---|---|
ctrlnum |
(MiAaPQ)5006524978 (Au-PeEL)EBL6524978 (OCoLC)1246184909 |
collection |
bib_alma |
record_format |
marc |
spelling |
Groote, Jan Friso. Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. 1st ed. Cham : Springer International Publishing AG, 2021. ©2021. 1 online resource (476 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.12652 Intro -- ETAPS Foreword -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Verification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- 1 Introduction -- 2 Preliminaries -- 3 Directed Search Algorithms -- 4 Directed Reachability -- 4.1 Distance Under-approximations -- 4.2 From Petri Net Relaxations to Distance Under-approximations -- 4.3 Directed Reachability Based on Distance Under-approximations -- 5 Experimental Results -- References -- Bridging Arrays and ADTs in Recursive Proofs -- 1 Introduction -- 2 Preliminaries -- 3 Synthesis of Recursive Relational Invariants -- 3.1 Overview -- 3.2 Classifying Operations -- 4 Recipe 1: Linear Scan -- 4.1 Motivating Example -- 4.2 Algorithm Description -- 5 Recipe 2: Noop-based synthesis -- 5.1 Motivating Example -- 5.2 Algorithm details -- 6 Evaluation -- 7 Related Work -- 8 Conclusion and Outlook -- References -- A Two-Phase Approach forConditional Floating-Point Verification -- 1 Introduction -- 2 A Two-Phase Approach -- 2.1 First Phase: Whole Program Analysis -- 2.2 Second Phase: Numerical Kernel Analysis -- 2.3 Soundness Guarantees -- 3 First Phase: Whole Program Analysis -- 4 Second Phase: Static Analysis with Daisy and CBMC -- 5 State of the Art on Real-World Programs -- 6 Evaluation of our Two-Phase Approach -- 7 Related Work -- 8 Conclusion -- Acknowledgements -- References -- Symbolic Coloured SCC Decomposition -- 1 Introduction -- 1.1 Related Work -- 2 Problem Definition -- 2.1 Graphs and Strongly Connected Components -- 2.2 Coloured SCC Decomposition Problem -- 3 Algorithm -- 3.1 Symbolic Computation Model -- 3.2 Forward-backward Algorithm -- 3.3 Lock-step Algorithm -- 3.4 Coloured Lock-step Algorithm -- 3.5 Correctness and Complexity of the Coloured Lock-step Algorithm -- 4 Experimental Evaluation -- 4.1 Implementation -- 4.2 Experiments. 5 Conclusions -- References -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- 1 Introduction -- 2 Background -- 2.1 Constraint Optimization Program (COP) -- 2.2 The Cell Placement Problem -- 2.2.1 Constraint Optimization Program for Cell Placement -- 2.3 Solving COP with SAT -- 2.3.1 Bit-vector Solving and SAT. -- 2.3.2 Extending Bit-vector Solving to Optimization. -- 2.4 Local Search Algorithms -- 2.4.1 Basic Local Search Strategy. -- 2.4.2 Neighbourhood Functions. -- 2.4.3 Advanced Versions of Local Search -- 3 Local Search with SAT Oracle (LSSO) -- 4 LSSO Algorithms for the Cell Placement Problem -- 4.1 Neighbourhood Generators -- 4.1.1 Neighbourhood Generator -- 4.1.2 N₂: a Family of Neighbourhood Generators -- 4.1.3 Hill-climbing Neighbourhood Generator N₃. -- 4.2 LSSO-based Algorithms for Placement -- 5 Experimental Results -- 6 Conclusion -- References -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- 1 Introduction -- 1.1 Proof of Concept -- 1.2 Detecting Intra-update Sniping Vulnerabilities -- 2 A Model for Infrastructure as Code -- 2.1 CloudFormation Infrastructures -- 2.2 Model of a CloudFormation Infrastructure -- 2.3 Execution Semantics -- 2.4 Upgrade Semantics and Security Policy -- 3 Architectural Design of the Hayha Tool -- 3.1 Upgrade States -- 3.2 Splitting Dependencies -- 3.3 Finding Vulnerabilities -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- Acknowledgement -- References -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- 1 Introduction -- 2 Preliminaries -- 3 Formulas -- 4 Certificates -- 5 FORTify -- 6 FORT-h -- 7 Experiments -- 8 Conclusion -- References -- Syntax-Guided Quantifier Instantiation -- 1 Introduction -- 2 Background -- 3 SyGuS Quantifier Instantiation (SyQI) -- 3.1 Grammar Construction. 3.2 Implementation Details -- 4 Experiments -- 5 Conclusion -- References -- Making Theory Reasoning Simpler -- 1 Introduction -- 2 Preliminaries and Related Work -- 3 Gaussian variable elimination -- 4 Arithmetic subterm generalization -- 5 Evaluation -- 6 Cancellation -- 7 Experimental evaluation -- 8 Conclusion -- References -- Deductive Stability Proofs for Ordinary Differential Equations -- 1 Introduction -- 2 Background: Di erential Dynamic Logic -- 3 Asymptotic Stability of an Equilibrium Point -- 3.1 Mathematical Preliminaries -- 3.2 Formal Specification -- 3.3 Lyapunov Functions -- 3.4 Asymptotic Stability Variations -- 4 General Stability -- 4.1 General Stability and General Attractivity -- 4.2 Specialization -- 5 Stability in KeYmaera X -- 6 Related Work -- 7 Conclusion -- References -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- 1 Introduction -- 2 Background -- 3 Extending Reluplex to Support Sign Constraints -- 4 Optimizations -- 5 Implementation -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- Acknowledgements. -- References -- cake_lpr: Verified Propagation Redundancy Checking in CakeML -- 1 Introduction -- 2 Background -- 2.1 HOL4 and CakeML -- 2.2 SAT Problems and Clausal Proofs -- 3 Linear Propagation Redundancy -- 4 CakeML Proof Checking -- 4.1 Verification Strategy -- 4.2 Verified Optimizations -- 5 Benchmarks -- 5.1 SaDiCaL PR Benchmarks -- 5.2 SAT Race 2019 Benchmarks -- 5.3 Mutilated Chessboard RAT Microbenchmarks -- 6 Related Work -- 7 Conclusion -- Acknowledgments. -- A Correctness Theorem for cake_lpr -- References -- Deductive Verification of Floating-Point Java Programs in KeY -- 1 Introduction -- 2 Background -- 2.1 Introduction to KeY -- 2.2 Floating-Point Arithmetic in Java -- 3 Floating-Point Support in KeY -- 3.1 Arithmetics -- 3.2 Transcendental Functions -- 4 Evaluation. 4.1 Benchmark Programs -- 4.2 Proof Obligation Generation -- 4.3 Evaluation of SMT Floating-Point Support -- 4.4 Evaluation of Support for Transcendental Functions in KeY -- 4.5 Discussion and insights -- 5 Related Work -- 6 Conclusion -- Acknowledgements -- References -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- 1 Introduction -- 2 Overview of Helmholtz and Michelson -- 2.1 Helmholtz -- 2.2 An Example Contract in Michelson -- 2.3 Specification -- 3 Refinement Type System for Mini-Michelson -- 3.1 Operational Semantics -- 3.2 Refinement Type System -- 4 Tool Implementation -- 4.1 Annotations -- 4.2 Case Study: Contract with Signature Verification -- 4.3 Experiments -- 5 Related Work -- 6 Conclusion -- References -- SyReNN: A Tool for Analyzing Deep Neural Networks -- 1 Introduction -- 2 Preliminaries -- 3 A Symbolic Representation of DNNs -- 4 Computing the Symbolic Representation -- 4.1 Algorithm for Extend -- 4.2 Representing Polytopes -- 5 SyReNN tool -- 6 Applications of SyReNN -- 6.1 Integrated Gradients -- 6.2 Visualization of DNN Decision Boundaries -- 6.3 Patching of DNNs -- 7 Related Work -- 8 Conclusion and Future Work -- References -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- 1 Introduction -- 2 Background -- 2.1 A Brief Overview of Algorithm Selection -- 2.2 Supervised Learning, Adaptive Boosting, Curse of Dimensionality, and K-Fold Cross-Validation -- 2.3 Unsupervised Learning and Principal Component Analysis -- 3 An overview of MachSMT -- 3.1 Features, Preprocessing, and Learning -- 3.2 Variants of MachSMT -- 3.3 Using MachSMT -- 3.4 User-defined Features -- 4 Experimental Evaluation of MachSMT on SMT-COMP 2019 and 2020 Data -- 4.1 Experimental Setup and Methodology -- 4.2 Experimental Results -- 5 Analysis and Discussion of Results -- 6 Related Work. 6.1 Key di erences between SATZilla and MachSMT -- 6.2 Algorithm Selection for Logic Solvers and Their Applications -- 7 Conclusions and Future Work -- References -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- 1 Introduction -- 2 Decision tree learning for controller representation -- 3 Tool -- 4 Predicate domain -- 4.1 Categorical predicates -- 4.2 Algebraic predicates -- 5 Predicate selection -- 6 New insights about determinization -- 7 Experiments -- 8 Conclusion -- References -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- 1 Introduction -- 2 The HLola Tool -- 3 Example Specifications -- References -- AMulet 2.0 for Verifying Multiplier Circuits -- 1 Introduction -- 2 Circuit Verification using Computer Algebra -- 3 Usage -- 4 AMulet 2.0 -- 5 Evaluation -- 6 Conclusion -- References -- RTLola on Board: Testing Real Driving Emissions on your Phone -- 1 Introduction -- 2 RDE Monitoring on Android -- 3 User Experience -- 4 Conclusion -- References -- Replicating Restart with ProlongedRetrials: An Experimental Report -- 1 Introduction -- 2 Restart with Prolonged Retrials -- 3 Experiments -- 4 Conclusion -- References -- A Web Interface for Petri Nets with Transits and Petri Games -- 1 Introduction -- 2 Web Interface for Petri Nets with Transits -- 3 Web Interface for Petri Games -- 4 Implementation Details -- 5 Conclusion -- References -- Momba: JANI Meets Python -- 1 Introduction -- 2 Scenario-Based Model Construction -- 3 Validation by Simulation -- 4 Harvesting the Benefits -- 5 Conclusion -- References -- SV-Comp Tool Competition Papers -- Software Verification: 10th Comparative Evaluation (SV-COMP 2021) -- 1 Introduction -- 2 Organization, Definitions, Formats, and Rules -- 3 Reproducibility -- 4 Results and Discussion -- 5 Conclusion. References. 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. Larsen, Kim Guldstrand. Print version: Groote, Jan Friso Tools and Algorithms for the Construction and Analysis of Systems Cham : Springer International Publishing AG,c2021 9783030720124 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6524978 Click to View |
language |
English |
format |
eBook |
author |
Groote, Jan Friso. |
spellingShingle |
Groote, Jan Friso. Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Lecture Notes in Computer Science Series ; Intro -- ETAPS Foreword -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Verification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- 1 Introduction -- 2 Preliminaries -- 3 Directed Search Algorithms -- 4 Directed Reachability -- 4.1 Distance Under-approximations -- 4.2 From Petri Net Relaxations to Distance Under-approximations -- 4.3 Directed Reachability Based on Distance Under-approximations -- 5 Experimental Results -- References -- Bridging Arrays and ADTs in Recursive Proofs -- 1 Introduction -- 2 Preliminaries -- 3 Synthesis of Recursive Relational Invariants -- 3.1 Overview -- 3.2 Classifying Operations -- 4 Recipe 1: Linear Scan -- 4.1 Motivating Example -- 4.2 Algorithm Description -- 5 Recipe 2: Noop-based synthesis -- 5.1 Motivating Example -- 5.2 Algorithm details -- 6 Evaluation -- 7 Related Work -- 8 Conclusion and Outlook -- References -- A Two-Phase Approach forConditional Floating-Point Verification -- 1 Introduction -- 2 A Two-Phase Approach -- 2.1 First Phase: Whole Program Analysis -- 2.2 Second Phase: Numerical Kernel Analysis -- 2.3 Soundness Guarantees -- 3 First Phase: Whole Program Analysis -- 4 Second Phase: Static Analysis with Daisy and CBMC -- 5 State of the Art on Real-World Programs -- 6 Evaluation of our Two-Phase Approach -- 7 Related Work -- 8 Conclusion -- Acknowledgements -- References -- Symbolic Coloured SCC Decomposition -- 1 Introduction -- 1.1 Related Work -- 2 Problem Definition -- 2.1 Graphs and Strongly Connected Components -- 2.2 Coloured SCC Decomposition Problem -- 3 Algorithm -- 3.1 Symbolic Computation Model -- 3.2 Forward-backward Algorithm -- 3.3 Lock-step Algorithm -- 3.4 Coloured Lock-step Algorithm -- 3.5 Correctness and Complexity of the Coloured Lock-step Algorithm -- 4 Experimental Evaluation -- 4.1 Implementation -- 4.2 Experiments. 5 Conclusions -- References -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- 1 Introduction -- 2 Background -- 2.1 Constraint Optimization Program (COP) -- 2.2 The Cell Placement Problem -- 2.2.1 Constraint Optimization Program for Cell Placement -- 2.3 Solving COP with SAT -- 2.3.1 Bit-vector Solving and SAT. -- 2.3.2 Extending Bit-vector Solving to Optimization. -- 2.4 Local Search Algorithms -- 2.4.1 Basic Local Search Strategy. -- 2.4.2 Neighbourhood Functions. -- 2.4.3 Advanced Versions of Local Search -- 3 Local Search with SAT Oracle (LSSO) -- 4 LSSO Algorithms for the Cell Placement Problem -- 4.1 Neighbourhood Generators -- 4.1.1 Neighbourhood Generator -- 4.1.2 N₂: a Family of Neighbourhood Generators -- 4.1.3 Hill-climbing Neighbourhood Generator N₃. -- 4.2 LSSO-based Algorithms for Placement -- 5 Experimental Results -- 6 Conclusion -- References -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- 1 Introduction -- 1.1 Proof of Concept -- 1.2 Detecting Intra-update Sniping Vulnerabilities -- 2 A Model for Infrastructure as Code -- 2.1 CloudFormation Infrastructures -- 2.2 Model of a CloudFormation Infrastructure -- 2.3 Execution Semantics -- 2.4 Upgrade Semantics and Security Policy -- 3 Architectural Design of the Hayha Tool -- 3.1 Upgrade States -- 3.2 Splitting Dependencies -- 3.3 Finding Vulnerabilities -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- Acknowledgement -- References -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- 1 Introduction -- 2 Preliminaries -- 3 Formulas -- 4 Certificates -- 5 FORTify -- 6 FORT-h -- 7 Experiments -- 8 Conclusion -- References -- Syntax-Guided Quantifier Instantiation -- 1 Introduction -- 2 Background -- 3 SyGuS Quantifier Instantiation (SyQI) -- 3.1 Grammar Construction. 3.2 Implementation Details -- 4 Experiments -- 5 Conclusion -- References -- Making Theory Reasoning Simpler -- 1 Introduction -- 2 Preliminaries and Related Work -- 3 Gaussian variable elimination -- 4 Arithmetic subterm generalization -- 5 Evaluation -- 6 Cancellation -- 7 Experimental evaluation -- 8 Conclusion -- References -- Deductive Stability Proofs for Ordinary Differential Equations -- 1 Introduction -- 2 Background: Di erential Dynamic Logic -- 3 Asymptotic Stability of an Equilibrium Point -- 3.1 Mathematical Preliminaries -- 3.2 Formal Specification -- 3.3 Lyapunov Functions -- 3.4 Asymptotic Stability Variations -- 4 General Stability -- 4.1 General Stability and General Attractivity -- 4.2 Specialization -- 5 Stability in KeYmaera X -- 6 Related Work -- 7 Conclusion -- References -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- 1 Introduction -- 2 Background -- 3 Extending Reluplex to Support Sign Constraints -- 4 Optimizations -- 5 Implementation -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- Acknowledgements. -- References -- cake_lpr: Verified Propagation Redundancy Checking in CakeML -- 1 Introduction -- 2 Background -- 2.1 HOL4 and CakeML -- 2.2 SAT Problems and Clausal Proofs -- 3 Linear Propagation Redundancy -- 4 CakeML Proof Checking -- 4.1 Verification Strategy -- 4.2 Verified Optimizations -- 5 Benchmarks -- 5.1 SaDiCaL PR Benchmarks -- 5.2 SAT Race 2019 Benchmarks -- 5.3 Mutilated Chessboard RAT Microbenchmarks -- 6 Related Work -- 7 Conclusion -- Acknowledgments. -- A Correctness Theorem for cake_lpr -- References -- Deductive Verification of Floating-Point Java Programs in KeY -- 1 Introduction -- 2 Background -- 2.1 Introduction to KeY -- 2.2 Floating-Point Arithmetic in Java -- 3 Floating-Point Support in KeY -- 3.1 Arithmetics -- 3.2 Transcendental Functions -- 4 Evaluation. 4.1 Benchmark Programs -- 4.2 Proof Obligation Generation -- 4.3 Evaluation of SMT Floating-Point Support -- 4.4 Evaluation of Support for Transcendental Functions in KeY -- 4.5 Discussion and insights -- 5 Related Work -- 6 Conclusion -- Acknowledgements -- References -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- 1 Introduction -- 2 Overview of Helmholtz and Michelson -- 2.1 Helmholtz -- 2.2 An Example Contract in Michelson -- 2.3 Specification -- 3 Refinement Type System for Mini-Michelson -- 3.1 Operational Semantics -- 3.2 Refinement Type System -- 4 Tool Implementation -- 4.1 Annotations -- 4.2 Case Study: Contract with Signature Verification -- 4.3 Experiments -- 5 Related Work -- 6 Conclusion -- References -- SyReNN: A Tool for Analyzing Deep Neural Networks -- 1 Introduction -- 2 Preliminaries -- 3 A Symbolic Representation of DNNs -- 4 Computing the Symbolic Representation -- 4.1 Algorithm for Extend -- 4.2 Representing Polytopes -- 5 SyReNN tool -- 6 Applications of SyReNN -- 6.1 Integrated Gradients -- 6.2 Visualization of DNN Decision Boundaries -- 6.3 Patching of DNNs -- 7 Related Work -- 8 Conclusion and Future Work -- References -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- 1 Introduction -- 2 Background -- 2.1 A Brief Overview of Algorithm Selection -- 2.2 Supervised Learning, Adaptive Boosting, Curse of Dimensionality, and K-Fold Cross-Validation -- 2.3 Unsupervised Learning and Principal Component Analysis -- 3 An overview of MachSMT -- 3.1 Features, Preprocessing, and Learning -- 3.2 Variants of MachSMT -- 3.3 Using MachSMT -- 3.4 User-defined Features -- 4 Experimental Evaluation of MachSMT on SMT-COMP 2019 and 2020 Data -- 4.1 Experimental Setup and Methodology -- 4.2 Experimental Results -- 5 Analysis and Discussion of Results -- 6 Related Work. 6.1 Key di erences between SATZilla and MachSMT -- 6.2 Algorithm Selection for Logic Solvers and Their Applications -- 7 Conclusions and Future Work -- References -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- 1 Introduction -- 2 Decision tree learning for controller representation -- 3 Tool -- 4 Predicate domain -- 4.1 Categorical predicates -- 4.2 Algebraic predicates -- 5 Predicate selection -- 6 New insights about determinization -- 7 Experiments -- 8 Conclusion -- References -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- 1 Introduction -- 2 The HLola Tool -- 3 Example Specifications -- References -- AMulet 2.0 for Verifying Multiplier Circuits -- 1 Introduction -- 2 Circuit Verification using Computer Algebra -- 3 Usage -- 4 AMulet 2.0 -- 5 Evaluation -- 6 Conclusion -- References -- RTLola on Board: Testing Real Driving Emissions on your Phone -- 1 Introduction -- 2 RDE Monitoring on Android -- 3 User Experience -- 4 Conclusion -- References -- Replicating Restart with ProlongedRetrials: An Experimental Report -- 1 Introduction -- 2 Restart with Prolonged Retrials -- 3 Experiments -- 4 Conclusion -- References -- A Web Interface for Petri Nets with Transits and Petri Games -- 1 Introduction -- 2 Web Interface for Petri Nets with Transits -- 3 Web Interface for Petri Games -- 4 Implementation Details -- 5 Conclusion -- References -- Momba: JANI Meets Python -- 1 Introduction -- 2 Scenario-Based Model Construction -- 3 Validation by Simulation -- 4 Harvesting the Benefits -- 5 Conclusion -- References -- SV-Comp Tool Competition Papers -- Software Verification: 10th Comparative Evaluation (SV-COMP 2021) -- 1 Introduction -- 2 Organization, Definitions, Formats, and Rules -- 3 Reproducibility -- 4 Results and Discussion -- 5 Conclusion. References. |
author_facet |
Groote, Jan Friso. Larsen, Kim Guldstrand. |
author_variant |
j f g jf jfg |
author2 |
Larsen, Kim Guldstrand. |
author2_variant |
k g l kg kgl |
author2_role |
TeilnehmendeR |
author_sort |
Groote, Jan Friso. |
title |
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. |
title_sub |
27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. |
title_full |
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. |
title_fullStr |
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. |
title_full_unstemmed |
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. |
title_auth |
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, 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 : 27th international conference, tacas 2021, held as part of the european joint conferences on theory and practice of software, etaps 2021, luxembourg city, luxembourg, march 27 - april 1, 2021, proceedings, part ii. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2021 |
physical |
1 online resource (476 pages) |
edition |
1st ed. |
contents |
Intro -- ETAPS Foreword -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Verification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- 1 Introduction -- 2 Preliminaries -- 3 Directed Search Algorithms -- 4 Directed Reachability -- 4.1 Distance Under-approximations -- 4.2 From Petri Net Relaxations to Distance Under-approximations -- 4.3 Directed Reachability Based on Distance Under-approximations -- 5 Experimental Results -- References -- Bridging Arrays and ADTs in Recursive Proofs -- 1 Introduction -- 2 Preliminaries -- 3 Synthesis of Recursive Relational Invariants -- 3.1 Overview -- 3.2 Classifying Operations -- 4 Recipe 1: Linear Scan -- 4.1 Motivating Example -- 4.2 Algorithm Description -- 5 Recipe 2: Noop-based synthesis -- 5.1 Motivating Example -- 5.2 Algorithm details -- 6 Evaluation -- 7 Related Work -- 8 Conclusion and Outlook -- References -- A Two-Phase Approach forConditional Floating-Point Verification -- 1 Introduction -- 2 A Two-Phase Approach -- 2.1 First Phase: Whole Program Analysis -- 2.2 Second Phase: Numerical Kernel Analysis -- 2.3 Soundness Guarantees -- 3 First Phase: Whole Program Analysis -- 4 Second Phase: Static Analysis with Daisy and CBMC -- 5 State of the Art on Real-World Programs -- 6 Evaluation of our Two-Phase Approach -- 7 Related Work -- 8 Conclusion -- Acknowledgements -- References -- Symbolic Coloured SCC Decomposition -- 1 Introduction -- 1.1 Related Work -- 2 Problem Definition -- 2.1 Graphs and Strongly Connected Components -- 2.2 Coloured SCC Decomposition Problem -- 3 Algorithm -- 3.1 Symbolic Computation Model -- 3.2 Forward-backward Algorithm -- 3.3 Lock-step Algorithm -- 3.4 Coloured Lock-step Algorithm -- 3.5 Correctness and Complexity of the Coloured Lock-step Algorithm -- 4 Experimental Evaluation -- 4.1 Implementation -- 4.2 Experiments. 5 Conclusions -- References -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- 1 Introduction -- 2 Background -- 2.1 Constraint Optimization Program (COP) -- 2.2 The Cell Placement Problem -- 2.2.1 Constraint Optimization Program for Cell Placement -- 2.3 Solving COP with SAT -- 2.3.1 Bit-vector Solving and SAT. -- 2.3.2 Extending Bit-vector Solving to Optimization. -- 2.4 Local Search Algorithms -- 2.4.1 Basic Local Search Strategy. -- 2.4.2 Neighbourhood Functions. -- 2.4.3 Advanced Versions of Local Search -- 3 Local Search with SAT Oracle (LSSO) -- 4 LSSO Algorithms for the Cell Placement Problem -- 4.1 Neighbourhood Generators -- 4.1.1 Neighbourhood Generator -- 4.1.2 N₂: a Family of Neighbourhood Generators -- 4.1.3 Hill-climbing Neighbourhood Generator N₃. -- 4.2 LSSO-based Algorithms for Placement -- 5 Experimental Results -- 6 Conclusion -- References -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- 1 Introduction -- 1.1 Proof of Concept -- 1.2 Detecting Intra-update Sniping Vulnerabilities -- 2 A Model for Infrastructure as Code -- 2.1 CloudFormation Infrastructures -- 2.2 Model of a CloudFormation Infrastructure -- 2.3 Execution Semantics -- 2.4 Upgrade Semantics and Security Policy -- 3 Architectural Design of the Hayha Tool -- 3.1 Upgrade States -- 3.2 Splitting Dependencies -- 3.3 Finding Vulnerabilities -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- Acknowledgement -- References -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- 1 Introduction -- 2 Preliminaries -- 3 Formulas -- 4 Certificates -- 5 FORTify -- 6 FORT-h -- 7 Experiments -- 8 Conclusion -- References -- Syntax-Guided Quantifier Instantiation -- 1 Introduction -- 2 Background -- 3 SyGuS Quantifier Instantiation (SyQI) -- 3.1 Grammar Construction. 3.2 Implementation Details -- 4 Experiments -- 5 Conclusion -- References -- Making Theory Reasoning Simpler -- 1 Introduction -- 2 Preliminaries and Related Work -- 3 Gaussian variable elimination -- 4 Arithmetic subterm generalization -- 5 Evaluation -- 6 Cancellation -- 7 Experimental evaluation -- 8 Conclusion -- References -- Deductive Stability Proofs for Ordinary Differential Equations -- 1 Introduction -- 2 Background: Di erential Dynamic Logic -- 3 Asymptotic Stability of an Equilibrium Point -- 3.1 Mathematical Preliminaries -- 3.2 Formal Specification -- 3.3 Lyapunov Functions -- 3.4 Asymptotic Stability Variations -- 4 General Stability -- 4.1 General Stability and General Attractivity -- 4.2 Specialization -- 5 Stability in KeYmaera X -- 6 Related Work -- 7 Conclusion -- References -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- 1 Introduction -- 2 Background -- 3 Extending Reluplex to Support Sign Constraints -- 4 Optimizations -- 5 Implementation -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- Acknowledgements. -- References -- cake_lpr: Verified Propagation Redundancy Checking in CakeML -- 1 Introduction -- 2 Background -- 2.1 HOL4 and CakeML -- 2.2 SAT Problems and Clausal Proofs -- 3 Linear Propagation Redundancy -- 4 CakeML Proof Checking -- 4.1 Verification Strategy -- 4.2 Verified Optimizations -- 5 Benchmarks -- 5.1 SaDiCaL PR Benchmarks -- 5.2 SAT Race 2019 Benchmarks -- 5.3 Mutilated Chessboard RAT Microbenchmarks -- 6 Related Work -- 7 Conclusion -- Acknowledgments. -- A Correctness Theorem for cake_lpr -- References -- Deductive Verification of Floating-Point Java Programs in KeY -- 1 Introduction -- 2 Background -- 2.1 Introduction to KeY -- 2.2 Floating-Point Arithmetic in Java -- 3 Floating-Point Support in KeY -- 3.1 Arithmetics -- 3.2 Transcendental Functions -- 4 Evaluation. 4.1 Benchmark Programs -- 4.2 Proof Obligation Generation -- 4.3 Evaluation of SMT Floating-Point Support -- 4.4 Evaluation of Support for Transcendental Functions in KeY -- 4.5 Discussion and insights -- 5 Related Work -- 6 Conclusion -- Acknowledgements -- References -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- 1 Introduction -- 2 Overview of Helmholtz and Michelson -- 2.1 Helmholtz -- 2.2 An Example Contract in Michelson -- 2.3 Specification -- 3 Refinement Type System for Mini-Michelson -- 3.1 Operational Semantics -- 3.2 Refinement Type System -- 4 Tool Implementation -- 4.1 Annotations -- 4.2 Case Study: Contract with Signature Verification -- 4.3 Experiments -- 5 Related Work -- 6 Conclusion -- References -- SyReNN: A Tool for Analyzing Deep Neural Networks -- 1 Introduction -- 2 Preliminaries -- 3 A Symbolic Representation of DNNs -- 4 Computing the Symbolic Representation -- 4.1 Algorithm for Extend -- 4.2 Representing Polytopes -- 5 SyReNN tool -- 6 Applications of SyReNN -- 6.1 Integrated Gradients -- 6.2 Visualization of DNN Decision Boundaries -- 6.3 Patching of DNNs -- 7 Related Work -- 8 Conclusion and Future Work -- References -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- 1 Introduction -- 2 Background -- 2.1 A Brief Overview of Algorithm Selection -- 2.2 Supervised Learning, Adaptive Boosting, Curse of Dimensionality, and K-Fold Cross-Validation -- 2.3 Unsupervised Learning and Principal Component Analysis -- 3 An overview of MachSMT -- 3.1 Features, Preprocessing, and Learning -- 3.2 Variants of MachSMT -- 3.3 Using MachSMT -- 3.4 User-defined Features -- 4 Experimental Evaluation of MachSMT on SMT-COMP 2019 and 2020 Data -- 4.1 Experimental Setup and Methodology -- 4.2 Experimental Results -- 5 Analysis and Discussion of Results -- 6 Related Work. 6.1 Key di erences between SATZilla and MachSMT -- 6.2 Algorithm Selection for Logic Solvers and Their Applications -- 7 Conclusions and Future Work -- References -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- 1 Introduction -- 2 Decision tree learning for controller representation -- 3 Tool -- 4 Predicate domain -- 4.1 Categorical predicates -- 4.2 Algebraic predicates -- 5 Predicate selection -- 6 New insights about determinization -- 7 Experiments -- 8 Conclusion -- References -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- 1 Introduction -- 2 The HLola Tool -- 3 Example Specifications -- References -- AMulet 2.0 for Verifying Multiplier Circuits -- 1 Introduction -- 2 Circuit Verification using Computer Algebra -- 3 Usage -- 4 AMulet 2.0 -- 5 Evaluation -- 6 Conclusion -- References -- RTLola on Board: Testing Real Driving Emissions on your Phone -- 1 Introduction -- 2 RDE Monitoring on Android -- 3 User Experience -- 4 Conclusion -- References -- Replicating Restart with ProlongedRetrials: An Experimental Report -- 1 Introduction -- 2 Restart with Prolonged Retrials -- 3 Experiments -- 4 Conclusion -- References -- A Web Interface for Petri Nets with Transits and Petri Games -- 1 Introduction -- 2 Web Interface for Petri Nets with Transits -- 3 Web Interface for Petri Games -- 4 Implementation Details -- 5 Conclusion -- References -- Momba: JANI Meets Python -- 1 Introduction -- 2 Scenario-Based Model Construction -- 3 Validation by Simulation -- 4 Harvesting the Benefits -- 5 Conclusion -- References -- SV-Comp Tool Competition Papers -- Software Verification: 10th Comparative Evaluation (SV-COMP 2021) -- 1 Introduction -- 2 Organization, Definitions, Formats, and Rules -- 3 Reproducibility -- 4 Results and Discussion -- 5 Conclusion. References. |
isbn |
9783030720131 9783030720124 |
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=6524978 |
illustrated |
Not Illustrated |
oclc_num |
1246184909 |
work_keys_str_mv |
AT grootejanfriso toolsandalgorithmsfortheconstructionandanalysisofsystems27thinternationalconferencetacas2021heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2021luxembourgcityluxembourgmarch27april12021proceedingspartii AT larsenkimguldstrand toolsandalgorithmsfortheconstructionandanalysisofsystems27thinternationalconferencetacas2021heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2021luxembourgcityluxembourgmarch27april12021proceedingspartii |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5006524978 (Au-PeEL)EBL6524978 (OCoLC)1246184909 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.12652 |
is_hierarchy_title |
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. |
container_title |
Lecture Notes in Computer Science Series ; v.12652 |
author2_original_writing_str_mv |
noLinkedField |
_version_ |
1792331059525844992 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11380nam a22004693i 4500</leader><controlfield tag="001">5006524978</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073839.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2021 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783030720131</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783030720124</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5006524978</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL6524978</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1246184909</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">Groote, Jan Friso.</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">27th International Conference, TACAS 2021, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, 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">2021.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2021.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (476 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.12652</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- ETAPS Foreword -- Preface -- Organization -- Contents - Part II -- Contents - Part I -- Verification Techniques (not SMT) -- Directed Reachability for Infinite-State Systems -- 1 Introduction -- 2 Preliminaries -- 3 Directed Search Algorithms -- 4 Directed Reachability -- 4.1 Distance Under-approximations -- 4.2 From Petri Net Relaxations to Distance Under-approximations -- 4.3 Directed Reachability Based on Distance Under-approximations -- 5 Experimental Results -- References -- Bridging Arrays and ADTs in Recursive Proofs -- 1 Introduction -- 2 Preliminaries -- 3 Synthesis of Recursive Relational Invariants -- 3.1 Overview -- 3.2 Classifying Operations -- 4 Recipe 1: Linear Scan -- 4.1 Motivating Example -- 4.2 Algorithm Description -- 5 Recipe 2: Noop-based synthesis -- 5.1 Motivating Example -- 5.2 Algorithm details -- 6 Evaluation -- 7 Related Work -- 8 Conclusion and Outlook -- References -- A Two-Phase Approach forConditional Floating-Point Verification -- 1 Introduction -- 2 A Two-Phase Approach -- 2.1 First Phase: Whole Program Analysis -- 2.2 Second Phase: Numerical Kernel Analysis -- 2.3 Soundness Guarantees -- 3 First Phase: Whole Program Analysis -- 4 Second Phase: Static Analysis with Daisy and CBMC -- 5 State of the Art on Real-World Programs -- 6 Evaluation of our Two-Phase Approach -- 7 Related Work -- 8 Conclusion -- Acknowledgements -- References -- Symbolic Coloured SCC Decomposition -- 1 Introduction -- 1.1 Related Work -- 2 Problem Definition -- 2.1 Graphs and Strongly Connected Components -- 2.2 Coloured SCC Decomposition Problem -- 3 Algorithm -- 3.1 Symbolic Computation Model -- 3.2 Forward-backward Algorithm -- 3.3 Lock-step Algorithm -- 3.4 Coloured Lock-step Algorithm -- 3.5 Correctness and Complexity of the Coloured Lock-step Algorithm -- 4 Experimental Evaluation -- 4.1 Implementation -- 4.2 Experiments.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">5 Conclusions -- References -- Case Studies -- Local Search with a SAT Oracle for Combinatorial Optimization -- 1 Introduction -- 2 Background -- 2.1 Constraint Optimization Program (COP) -- 2.2 The Cell Placement Problem -- 2.2.1 Constraint Optimization Program for Cell Placement -- 2.3 Solving COP with SAT -- 2.3.1 Bit-vector Solving and SAT. -- 2.3.2 Extending Bit-vector Solving to Optimization. -- 2.4 Local Search Algorithms -- 2.4.1 Basic Local Search Strategy. -- 2.4.2 Neighbourhood Functions. -- 2.4.3 Advanced Versions of Local Search -- 3 Local Search with SAT Oracle (LSSO) -- 4 LSSO Algorithms for the Cell Placement Problem -- 4.1 Neighbourhood Generators -- 4.1.1 Neighbourhood Generator -- 4.1.2 N₂: a Family of Neighbourhood Generators -- 4.1.3 Hill-climbing Neighbourhood Generator N₃. -- 4.2 LSSO-based Algorithms for Placement -- 5 Experimental Results -- 6 Conclusion -- References -- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities -- 1 Introduction -- 1.1 Proof of Concept -- 1.2 Detecting Intra-update Sniping Vulnerabilities -- 2 A Model for Infrastructure as Code -- 2.1 CloudFormation Infrastructures -- 2.2 Model of a CloudFormation Infrastructure -- 2.3 Execution Semantics -- 2.4 Upgrade Semantics and Security Policy -- 3 Architectural Design of the Hayha Tool -- 3.1 Upgrade States -- 3.2 Splitting Dependencies -- 3.3 Finding Vulnerabilities -- 4 Experiments -- 5 Related Work -- 6 Conclusion -- Acknowledgement -- References -- Proof Generation/Validation -- Certifying Proofs in the First-Order Theory of Rewriting -- 1 Introduction -- 2 Preliminaries -- 3 Formulas -- 4 Certificates -- 5 FORTify -- 6 FORT-h -- 7 Experiments -- 8 Conclusion -- References -- Syntax-Guided Quantifier Instantiation -- 1 Introduction -- 2 Background -- 3 SyGuS Quantifier Instantiation (SyQI) -- 3.1 Grammar Construction.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">3.2 Implementation Details -- 4 Experiments -- 5 Conclusion -- References -- Making Theory Reasoning Simpler -- 1 Introduction -- 2 Preliminaries and Related Work -- 3 Gaussian variable elimination -- 4 Arithmetic subterm generalization -- 5 Evaluation -- 6 Cancellation -- 7 Experimental evaluation -- 8 Conclusion -- References -- Deductive Stability Proofs for Ordinary Differential Equations -- 1 Introduction -- 2 Background: Di erential Dynamic Logic -- 3 Asymptotic Stability of an Equilibrium Point -- 3.1 Mathematical Preliminaries -- 3.2 Formal Specification -- 3.3 Lyapunov Functions -- 3.4 Asymptotic Stability Variations -- 4 General Stability -- 4.1 General Stability and General Attractivity -- 4.2 Specialization -- 5 Stability in KeYmaera X -- 6 Related Work -- 7 Conclusion -- References -- Tool Papers -- An SMT-Based Approach for Verifying Binarized Neural Networks -- 1 Introduction -- 2 Background -- 3 Extending Reluplex to Support Sign Constraints -- 4 Optimizations -- 5 Implementation -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- Acknowledgements. -- References -- cake_lpr: Verified Propagation Redundancy Checking in CakeML -- 1 Introduction -- 2 Background -- 2.1 HOL4 and CakeML -- 2.2 SAT Problems and Clausal Proofs -- 3 Linear Propagation Redundancy -- 4 CakeML Proof Checking -- 4.1 Verification Strategy -- 4.2 Verified Optimizations -- 5 Benchmarks -- 5.1 SaDiCaL PR Benchmarks -- 5.2 SAT Race 2019 Benchmarks -- 5.3 Mutilated Chessboard RAT Microbenchmarks -- 6 Related Work -- 7 Conclusion -- Acknowledgments. -- A Correctness Theorem for cake_lpr -- References -- Deductive Verification of Floating-Point Java Programs in KeY -- 1 Introduction -- 2 Background -- 2.1 Introduction to KeY -- 2.2 Floating-Point Arithmetic in Java -- 3 Floating-Point Support in KeY -- 3.1 Arithmetics -- 3.2 Transcendental Functions -- 4 Evaluation.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">4.1 Benchmark Programs -- 4.2 Proof Obligation Generation -- 4.3 Evaluation of SMT Floating-Point Support -- 4.4 Evaluation of Support for Transcendental Functions in KeY -- 4.5 Discussion and insights -- 5 Related Work -- 6 Conclusion -- Acknowledgements -- References -- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types -- 1 Introduction -- 2 Overview of Helmholtz and Michelson -- 2.1 Helmholtz -- 2.2 An Example Contract in Michelson -- 2.3 Specification -- 3 Refinement Type System for Mini-Michelson -- 3.1 Operational Semantics -- 3.2 Refinement Type System -- 4 Tool Implementation -- 4.1 Annotations -- 4.2 Case Study: Contract with Signature Verification -- 4.3 Experiments -- 5 Related Work -- 6 Conclusion -- References -- SyReNN: A Tool for Analyzing Deep Neural Networks -- 1 Introduction -- 2 Preliminaries -- 3 A Symbolic Representation of DNNs -- 4 Computing the Symbolic Representation -- 4.1 Algorithm for Extend -- 4.2 Representing Polytopes -- 5 SyReNN tool -- 6 Applications of SyReNN -- 6.1 Integrated Gradients -- 6.2 Visualization of DNN Decision Boundaries -- 6.3 Patching of DNNs -- 7 Related Work -- 8 Conclusion and Future Work -- References -- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers -- 1 Introduction -- 2 Background -- 2.1 A Brief Overview of Algorithm Selection -- 2.2 Supervised Learning, Adaptive Boosting, Curse of Dimensionality, and K-Fold Cross-Validation -- 2.3 Unsupervised Learning and Principal Component Analysis -- 3 An overview of MachSMT -- 3.1 Features, Preprocessing, and Learning -- 3.2 Variants of MachSMT -- 3.3 Using MachSMT -- 3.4 User-defined Features -- 4 Experimental Evaluation of MachSMT on SMT-COMP 2019 and 2020 Data -- 4.1 Experimental Setup and Methodology -- 4.2 Experimental Results -- 5 Analysis and Discussion of Results -- 6 Related Work.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">6.1 Key di erences between SATZilla and MachSMT -- 6.2 Algorithm Selection for Logic Solvers and Their Applications -- 7 Conclusions and Future Work -- References -- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts -- 1 Introduction -- 2 Decision tree learning for controller representation -- 3 Tool -- 4 Predicate domain -- 4.1 Categorical predicates -- 4.2 Algebraic predicates -- 5 Predicate selection -- 6 New insights about determinization -- 7 Experiments -- 8 Conclusion -- References -- Tool Demo Papers -- HLola: a Very Functional Tool for Extensible Stream Runtime Verification -- 1 Introduction -- 2 The HLola Tool -- 3 Example Specifications -- References -- AMulet 2.0 for Verifying Multiplier Circuits -- 1 Introduction -- 2 Circuit Verification using Computer Algebra -- 3 Usage -- 4 AMulet 2.0 -- 5 Evaluation -- 6 Conclusion -- References -- RTLola on Board: Testing Real Driving Emissions on your Phone -- 1 Introduction -- 2 RDE Monitoring on Android -- 3 User Experience -- 4 Conclusion -- References -- Replicating Restart with ProlongedRetrials: An Experimental Report -- 1 Introduction -- 2 Restart with Prolonged Retrials -- 3 Experiments -- 4 Conclusion -- References -- A Web Interface for Petri Nets with Transits and Petri Games -- 1 Introduction -- 2 Web Interface for Petri Nets with Transits -- 3 Web Interface for Petri Games -- 4 Implementation Details -- 5 Conclusion -- References -- Momba: JANI Meets Python -- 1 Introduction -- 2 Scenario-Based Model Construction -- 3 Validation by Simulation -- 4 Harvesting the Benefits -- 5 Conclusion -- References -- SV-Comp Tool Competition Papers -- Software Verification: 10th Comparative Evaluation (SV-COMP 2021) -- 1 Introduction -- 2 Organization, Definitions, Formats, and Rules -- 3 Reproducibility -- 4 Results and Discussion -- 5 Conclusion.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">References.</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">Larsen, Kim Guldstrand.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Groote, Jan Friso</subfield><subfield code="t">Tools and Algorithms for the Construction and Analysis of Systems</subfield><subfield code="d">Cham : Springer International Publishing AG,c2021</subfield><subfield code="z">9783030720124</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=6524978</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |