Tools and Algorithms for the Construction and Analysis of Systems
Description
More details
Content
Tool Demos.- EVA: a Tool for the Compositional Verification of AUTOSAR Models.- WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification.- Multiparty Session Typing in Java, Deductively.- PyLTA: A Verification Tool for Parameterized Distributed Algorithms.- FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format.- Eclipse ESCETT: The Eclipse Supervisory Control Engineering Toolkit.- Combinatorial Optimization/Theorem Proving.- New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization.- Verified reductions for optimization.- Specifying and Verifying Higher-order Rust Iterators.- Extending a High-Performance Prover to Higher-Order Logic.- Tools (Regular Papers).- The WhyRel Prototype for Relational Verification of Pointer Programs.- Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Converter.- CoPTIC: Constraint Programming Translated Into C.- Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability.- Synthesis.- Computing Adequately Permissive Assumptions for Synthesis.- Verification-guided Programmatic Controller Synthesis.- Taming Large Bounds in Synthesis from Bounded-Liveness Specifications.- Lockstep Composition for Unbalanced Loops.- Synthesis of Distributed Agreement-Based Systems with Effciently Decidable Verification.- LTL Reactive Synthesis with a Few Hints.- Timed Automata Verification and Synthesis via Finite Automata Learning.- Graphs/Probabilistic Systems.- A Truly Symbolic Linear-Time Algorithm for SCC Decomposition.- Transforming quantified Boolean formulas using biclique covers.- Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration.- Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants.- Runtime Monitoring/Program Analysis.- Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote.- Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis.- Explainable Online Monitoring of Metric Temporal Logic.- 12th Competition on Software Verification - SV-COMP 2023 .- Competition on Software Verification and Witness Validation: SV-COMP 2023.- Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation (Competition Contribution).- 2LS: Arrays and Loop Unwinding (Competition Contribution).- Bubaak: Runtime Monitoring of Program Verifiers (Competition Contribution).- EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution).- Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution).- Java Ranger: Supporting String and Array Operations (Competition Contribution).- Korn-Software Verification with Horn Clauses (Competition Contribution).- Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution).- PIChecker: A POR and Interpolation based Verifierfor Concurrent Programs (Competition Contribution).- Ultimate Automizer and the CommuHash Normal Form (Competition Contribution).- Ultimate Taipan and Race Detection in Ultimate (Competition Contribution).- VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution).- VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution).