Cover Image

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

Bibliographic Details
Main Author: Sankaranarayanan, Sriram.
Other Authors: Sharygina, Natasha.
Format: eBook
Language:English
Published: Cham : Springer International Publishing AG, 2023.
Edition:1st ed.
Series:Lecture Notes in Computer Science Series
Subjects:
Electronic books.
Online Access:Click to View
LEADER 11362nam a22004693i 4500
001 EBC7241009
003 MiAaPQ
005 20231204023228.0
006 m o d |
007 cr cnu||||||||
008 231204s2023 xx o ||||0 eng d
020 |a 9783031308239  |q (electronic bk.) 
020 |z 9783031308222 
035 |a (MiAaPQ)EBC7241009 
035 |a (Au-PeEL)EBL7241009 
035 |a (OCoLC)1377209777 
040 |a MiAaPQ  |b eng  |e rda  |e pn  |c MiAaPQ  |d MiAaPQ 
050 4 |a QA75.5-76.95 
100 1 |a Sankaranarayanan, Sriram. 
245 1 0 |a Tools and Algorithms for the Construction and Analysis of Systems :  |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 I. 
250 |a 1st ed. 
264 1 |a Cham :  |b Springer International Publishing AG,  |c 2023. 
264 4 |c ©2023. 
300 |a 1 online resource (718 pages) 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
490 1 |a Lecture Notes in Computer Science Series ;  |v v.13993 
505 0 |a Intro -- ETAPS Foreword -- Preface -- Organization -- Contents - Part I -- Contents - Part II -- Invited Talk -- A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems -- 1 Introduction -- 2 Preliminaries -- 2.1 Brief Overview of Martingale Theory -- 2.2 Problem Statement -- 3 Supermartingale Certificate Functions -- 4 Learner-Verifier Framework for Stochastic Systems -- 4.1 Algorithm Initialization -- 4.2 The Learner module -- 4.3 The Verifier module -- 5 Bounding Expected Values of Neural Networks -- 6 Discussion on Extension to General Certificates -- 7 Related Work -- 8 Conclusion -- References -- Model Checking -- Bounded Model Checking for Asynchronous Hyperproperties -- 1 Introduction -- 2 Extended Asynchronous HyperLTL -- 3 Bounded Model Checking for A-HLTL -- 3.1 Bounded Semantics of A-HLTL -- 3.2 From Bounded Semantics to QBF Solving -- 4 Complexity of A-HLTL Model Checking for AcyclicFrames -- 5 Case Studies and Evaluation -- 5.1 Analysis of Experimental Results -- 6 Conclusion and Future Work -- References -- Model Checking Linear Dynamical Systems under Floating-point Rounding -- 1 Introduction -- 2 Preliminaries -- 2.1 Linear dynamical systems and rounding functions -- 2.2 Model checking -- 2.3 Structure of M -- 3 Undecidability of point-to-point reachability -- 4 Pseudo-periodic orbits of non-negative LDS -- 4.1 Preprocessing periodicity -- 4.2 Pseudo-periodicity within top SCCs -- 4.3 Pseudo-periodicity within lower SCCs -- 5 Decidability of model checking -- Acknowledgements -- References -- Efficient Loop Conditions for Bounded Model Checking Hyperproperties -- 1 Introduction -- 2 Preliminaries -- 3 Adaptation of BMC to HyperLTL on Infinite Traces -- 4 Simulation-Based BMC Algorithms for HyperLTL -- 4.1 Encodings for EA-Simulation -- 4.2 Encodings for AE-Simulation. 
505 8 |a 4.3 Encodings for AE-Simulation with Prophecies -- 5 Implementation and Experiments -- 5.1 Case Studies and Empirical Evaluation -- 5.2 Analysis and Discussion -- 6 Conclusion and Future Work -- References -- Reconciling Preemption Bounding with DPOR -- 1 Introduction -- 2 Background -- 2.1 The Basics of Dynamic Partial Order Reduction -- 2.2 Bounded Partial Order Reduction -- 2.3 TruSt: Optimal Dynamic Partial Order Reduction -- 3 Bounded Optimal DPOR: Obstacles -- 3.1 Pessimistic Bound Definition -- 3.2 Need For Slack -- 4 Recovering Completeness via Slack -- 4.1 Properties of TruSt -- 4.2 Correctness of Slacked Bounding -- 5 Implementation -- 6 Evaluation -- 6.1 Bound and Bug Manifestation -- 6.2 Comparison with Plain DPOR on Safe Benchmarks -- 6.3 Bound Calculation Overhead -- 6.4 Overhead due to Bound-Blocked Executions -- 7 Related Work -- Acknowledgments -- 8 Data-Availability Statement -- References -- Optimal Stateless Model Checking for Causal Consistency -- 1 Introduction -- 2 Preliminaries -- 3 Causally Consistent Models -- 4 Trace Semantics -- 5 DPOR Algorithm for CC, CCv, CM -- 6 Experimental Evaluation -- 6.1 Litmus Benchmarks -- 6.2 SV-COMP Benchmarks -- 6.3 Database Applications -- 6.4 Classical Benchmarks -- 6.5 Parameterized Benchmarks -- 7 Conclusion -- 8 Data-Availability Statement -- References -- Symbolic Model Checking for TLA+ Made Faster -- 1 Introduction -- 2 Background -- 2.1 TLA+ -- 2.2 KerA+ -- 2.3 Abstract Reduction System -- 2.4 SMT Theory of Arrays -- 3 Encoding TLA+ using Arrays -- 3.1 Encoding TLA+ Sets using Arrays -- 3.2 Encoding TLA+ Functions using Arrays -- 3.3 Correctness of the Reduction to Arrays -- 4 Evaluation -- 4.1 Benchmarks -- 4.2 Results -- 5 Related Work -- 6 Conclusions -- Acknowledgements -- References -- AutoHyper: Explicit-State Model Checking for HyperLTL -- 1 Introduction -- 2 Preliminaries. 
505 8 |a 3 Automata-based HyperLTL Model Checking -- 3.1 Automata-based Verification -- 3.2 HyperLTL Model Checking by Language Inclusion -- 4 Related Work and HyperLTL Verification Approaches -- 5 AutoHyper: Tool Overview -- 6 HyperLTL Model Checking Complexity in Practice -- 6.1 Performance of Inclusion Checkers -- 6.2 Model Checking Beyond ∀∗∃∗ -- 7 Evaluation on Symbolic Systems -- 7.1 Model Checking GNI on Boolean Programs -- 7.2 Explicit Model Checking of Symbolic Systems -- 7.3 Hyperproperties for Path Planning -- 7.4 Bounded vs. Explicit-State Model Checking -- 8 Evaluating Strategy-based Verification -- 8.1 Effectiveness of Strategy-based Verification -- 8.2 Efficiency of Strategy-based Verification -- 9 Conclusion -- Acknowledgments -- Data Availability Statement -- References -- Machine Learning/Neural Networks -- Feature Necessity &amp -- Relevancyin ML Classifier Explanations -- 1 Introduction -- 2 Preliminaries -- 2.1 Classification Problems -- 2.2 Examples of Classifiers -- 2.3 Formal Explainability -- 3 Feature Relevancy &amp -- Necessity: Theory -- 3.1 Defining Necessity, Relevancy &amp -- Irrelevancy -- 3.2 Feature Necessity -- 3.3 Feature Relevancy: Membership Results -- 3.4 Feature Relevancy: Hardness Results -- 4 Feature Relevancy: Example Algorithms -- 4.1 Relevancy for d-DNNF Classifiers -- 4.2 Relevancy for Monotonic Classifiers -- 5 Experimental Results -- 6 Related Work -- 7 Conclusions -- Acknowledgements -- References -- Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks -- 1 Introduction -- 2 Background -- 3 Provable Approximations for Minimal Explanations -- 4 Finding Minimal Explanations Efficiently -- 5 Minimal Bundle Explanations -- 6 Evaluation -- 7 Related Work -- 8 Conclusion -- References -- OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks -- 1 Introduction. 
505 8 |a 2 Preliminaries -- 2.1 Deep Neural Networks and the Robustness -- 2.2 Occlusion Perturbation -- 3 The Occlusion Robustness Verification Problem -- 4 SMT-Based Occlusion Robustness Verification -- 4.1 A Naïve SMT Encoding Method -- 4.2 Our Encoding Approach -- 4.3 The Correctness of the Encoding -- 4.4 Verification Acceleration Techniques -- 5 Implementation and Evaluation -- 6 Related Work -- 7 Conclusion and Future Work -- Acknowledgments -- References -- Neural Network-Guided Synthesis of Recursive List Functions -- 1 Introduction -- 2 The Synthesis Problem -- 3 The Design and Training of the RNN -- 3.1 The Architecture of the RNN -- 3.2 Training the RNN -- 4 Synthesis Based on the Trained RNN -- 5 Implementation and Experiments -- 5.1 Dataset and predicates -- 5.2 Evaluation -- 6 Related Work -- 7 Conclusion -- Acknowledgments -- References -- Automata -- Modular Mix-and-Match Complementation of Buchi Automata -- 1 Introduction -- 2 Preliminaries -- 3 A Modular Complementation Algorithm -- 3.1 Basic Synchronous Algorithm -- 4 Modular Complementation of Elevator Automata -- 4.1 Complementation of Inherently Weak Accepting Components -- 4.2 Complementation of Deterministic Accepting Components -- 4.3 Upper-bound for Elevator Automata Complementation -- 5 Optimizations of the Modular Construction -- 5.1 Complementation of Initial Deterministic Partition Blocks -- 5.2 Postponed Construction -- 5.3 Round-Robin Algorithm -- 5.4 Shared Breakpoint -- 5.5 Simulation Pruning -- 6 Modular Complementation of Non-Elevator Automata -- 7 Experimental Evaluation -- 8 Related Work -- 9 Conclusion and Future Work -- References -- Validating Streaming JSON Documents with Learned VPAs -- 1 Introduction -- 2 Visibly Pushdown Languages -- 3 JSON Format -- 4 Validation of JSON Documents -- 5 Implementation and Experiments -- 6 Future Work -- References. 
505 8 |a Antichains Algorithms for the Inclusion Problem Between ω-VPL -- 1 Introduction -- 2 Background -- 3 Foundations -- 4 Fixpoint Characterization -- 5 Monotonicity Requirements -- 6 Quasiorders for ω-VPL -- 7 Algorithm -- 7.1 State-based Algorithm -- 8 Experiments -- 9 Conclusion and Future Work -- References -- Stack-Aware Hyperproperties -- 1 Introduction -- 2 Motivation -- 3 Stack-aware Hyper Computation Tree Logic (sHCTL*) -- 3.1 Pushdown Systems -- 3.2 Syntax of sHCTL* -- 3.3 Semantics of sHCTL* -- 4 A Decision Procedure for sHCTL* -- 4.1 Automata on Pushdown Alphabets -- 4.2 Algorithm for sHCTL* -- 5 Lower Bound -- 6 Conclusions -- References -- Proofs -- Propositional Proof Skeletons -- 1 Introduction -- 2 Background and Related Work -- 3 Problem Overview -- 4 Creating Proof Skeletons -- 4.1 Online Generation of Proof Skeletons -- 4.2 Offline Generation of Proof Skeletons -- 5 Reconstructing Proofs from Skeletons -- 5.1 Filling Skeletons Using Incremental Solvers -- 5.2 Shrinking Skeletons -- 5.3 Reconstructing LRAT Proofs from Skeletons -- 6 Experimental Evaluation -- 6.1 Single-Core Proof Reconstruction -- 6.2 Skeleton Compression Ratio -- 6.3 Impact of Reason Clauses in Online Skeletons -- 6.4 Impact of the UNSAT Core on Offline Skeletons -- 6.5 Skeleton Shrinking after Reconstruction -- 6.6 Comparison With Sequential and Parallel SAT Solvers -- 7 Conclusion -- References -- Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers -- 1 Introduction -- 2 Background and Related Work -- 3 Basic Proof Production -- 3.1 Solver Partial Proof Production -- 3.2 Partial Proof Combination -- 3.3 Proof Pruning -- 4 Distributed Proof Production -- 4.1 Overview -- 4.2 Distributed Pruning -- 4.3 Merging Step -- 5 Implementation -- 6 Evaluation -- 6.1 Experimental Setup -- 6.2 Results -- 7 Conclusion and Future Work -- Acknowledgments. 
505 8 |a References. 
588 |a Description based on publisher supplied metadata and other sources. 
590 |a Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2023. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries.  
655 4 |a Electronic books. 
700 1 |a Sharygina, Natasha. 
776 0 8 |i Print version:  |a Sankaranarayanan, Sriram  |t Tools and Algorithms for the Construction and Analysis of Systems  |d Cham : Springer International Publishing AG,c2023  |z 9783031308222 
797 2 |a ProQuest (Firm) 
830 0 |a Lecture Notes in Computer Science Series 
856 4 0 |u https://ebookcentral.proquest.com/lib/matrademy/detail.action?docID=7241009  |z Click to View 

Similar Items