TACAS 2021
56 papers
- A Flexible Proof Format for SAT Solver-Elaborator Communication
- A Game for Linear-time-Branching-time Spectroscopy
- A Two-Phase Approach for Conditional Floating-Point Verification
- A Web Interface for Petri Nets with Transits and Petri Games
- AMulet 2.0 for Verifying Multiplier Circuits
- Algebraic Quantitative Semantics for Efficient Online Temporal Monitoring
- An SMT-Based Approach for Verifying Binarized Neural Networks
- Analysis of Markov Jump Processes under Terminal Constraints
- Analyzing Infrastructure as Code to Prevent Intra-update Sniping Vulnerabilities
- Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
- Bounded Model Checking for Hyperproperties
- Bridging Arrays and ADTs in Recursive Proofs
- Certifying Proofs in the First-Order Theory of Rewriting
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution)
- Deductive Stability Proofs for Ordinary Differential Equations
- Deductive Verification of Floating-Point Java Programs in KeY
- Directed Reachability for Infinite-State Systems
- FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions
- Finding Provably Optimal Markov Chains
- Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)
- General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver
- Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints - (Competition Contribution)
- HLola: a Very Functional Tool for Extensible Stream Runtime Verification
- Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
- Improving Neural Network Verification through Spurious Region Guided Refinement
- Inductive Synthesis for Probabilistic Programs Reaches New Horizons
- Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
- Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
- JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution)
- Local Search with a SAT Oracle for Combinatorial Optimization
- MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
- Making Theory Reasoning Simpler
- Momba: JANI Meets Python
- Multi-objective Optimization of Long-run Average and Total Rewards
- Network Traffic Classification by Program Synthesis
- On Satisficing in Quantitative Games
- Probabilistic and Systematic Coverage of Consecutive Test-Method Pairs for Detecting Order-Dependent Flaky Tests
- Quasipolynomial Computation of Nested Fixpoints
- RTLola on Board: Testing Real Driving Emissions on your Phone
- Replicating sc Restart with Prolonged Retrials: An Experimental Report
- Resilient Capacity-Aware Routing
- SAT Solving with GPU Accelerated Inprocessing
- Software Verification: 10th Comparative Evaluation (SV-COMP 2021)
- SyReNN: A Tool for Analyzing Deep Neural Networks
- Symbiotic 8: Beyond Symbolic Execution - (Competition Contribution)
- Symbolic Coloured SCC Decomposition
- Syntax-Guided Quantifier Instantiation
- Synthesizing Context-free Grammars from Recurrent Neural Networks
- Timed Automata Relaxation for Reachability
- Towards String Support in JayHorn (Competition Contribution)
- VeriAbs: A Tool for Scalable Verification by Abstraction (Competition Contribution)
- cake_lpr: Verified Propagation Redundancy Checking in CakeML
- cpalockator: Thread-Modular Analysis with Projections - (Competition Contribution)
- dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts