TACAS 2023
77 papers
- 2LS: Arrays and Loop Unwinding - (Competition Contribution)
- A Formal CHERI-C Semantics for Verification
- A GPU Tree Database for Many-Core Explicit State Space Exploration
- A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems
- A Matrix-Based Approach to Parity Games
- A Practitioner's Guide to MDP Model Checking Algorithms
- A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
- ALASCA: Reasoning in Quantified Linear Arithmetic
- Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability
- Active Learning for SAT Solver Benchmarking
- Antichains Algorithms for the Inclusion Problem Between ømega-VPL
- AutoHyper: Explicit-State Model Checking for HyperLTL
- Automated Verification for Real-Time Systems - via Implicit Clocks and an Extended Antimirov Algorithm
- Bounded Model Checking for Asynchronous Hyperproperties
- Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator
- Bubaak: Runtime Monitoring of Program Verifiers - (Competition Contribution)
- Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format
- Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
- CoPTIC: Constraint Programming Translated Into C
- Competition on Software Verification and Witness Validation: SV-COMP 2023
- Computing Adequately Permissive Assumptions for Synthesis
- Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis
- Correct Approximation of Stationary Distributions
- EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs - (Competition Contribution)
- EVA: a Tool for the Compositional Verification of AUTOSAR Models
- Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit
- Efficient Loop Conditions for Bounded Model Checking Hyperproperties
- Explainable Online Monitoring of Metric Temporal Logic
- Extending a High-Performance Prover to Higher-Order Logic
- Feature Necessity & Relevancy in ML Classifier Explanations
- FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format
- Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution)
- Industrial-Strength Controlled Concurrency Testing for sc C tt # Programs with sc Coyote
- Inferring Needless Write Memory Accesses on Ethereum Bytecode
- Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution)
- Korn - Software Verification with Horn Clauses (Competition Contribution)
- LTL Reactive Synthesis with a Few Hints
- Lockstep Composition for Unbalanced Loops
- Make Flows Small Again: Revisiting the Flow Framework
- Model Checking Linear Dynamical Systems under Floating-point Rounding
- Modular Mix-and-Match Complementation of Büchi Automata
- Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)
- Multiparty Session Typing in Java, Deductively
- Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning
- Neural Network-Guided Synthesis of Recursive List Functions
- New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization
- OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks
- Optimal Stateless Model Checking for Causal Consistency
- PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution)
- ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
- Parameterized Verification under TSO with Data Types
- Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
- Propositional Proof Skeletons
- PyLTA: A Verification Tool for Parameterized Distributed Algorithms
- Reconciling Preemption Bounding with DPOR
- Robust Almost-Sure Reachability in Multi-Environment MDPs
- Specifying and Verifying Higher-order Rust Iterators
- Stack-Aware Hyperproperties
- Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution)
- Symbolic Model Checking for TLA+ Made Faster
- Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification
- Taming Large Bounds in Synthesis from Bounded-Liveness Specifications
- The Packing Chromatic Number of the Infinite Square Grid is 15
- The WhyRel Prototype for Modular Relational Verification of Pointer Programs
- Timed Automata Verification and Synthesis via Finite Automata Learning
- Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
- Transforming Quantified Boolean Formulas Using Biclique Covers
- Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution)
- Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution)
- Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
- Validating Streaming JSON Documents with Learned VPAs
- VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution)
- VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution)
- Verification-guided Programmatic Controller Synthesis
- Verified reductions for optimization
- Verifying Learning-Based Robotic Navigation Systems
- WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification