TACAS 2022
67 papers
- A Direct Symbolic Algorithm for Solving Stochastic Rabin Games
- A Max-SMT Superoptimizer for EVM handling Memory and Storage
- A New Approach for Active Automata Learning Based on Apartness
- A Probabilistic Logic for Verifying Continuous-time Markov Chains
- A Prototype for Data Race Detection in CSeq 3 - (Competition Contribution)
- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic
- A Theoretical Analysis of Random Regression Test Prioritization
- AProVE: Non-Termination Witnesses for C Programs - (Competition Contribution)
- Adiar Binary Decision Diagrams in External Memory
- Alpinist: An Annotation-Aware GPU Program Optimizer
- Automated Translation of Natural Language Requirements to Runtime Monitors
- Automatic Repair for Network Programs
- BRICK: Path Enumeration Based Bounded Reachability Checking of C Program (Competition Contribution)
- Better Counterexamples for Dafny
- Clausal Proofs for Pseudo-Boolean Reasoning
- CoVeriTeam: On-Demand Composition of Cooperative Verification Systems
- Comparative Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems
- Correct Probabilistic Model Checking with Floating-Point Arithmetic
- Correlated Equilibria and Fairness in Concurrent Stochastic Games
- Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)
- Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)
- Distributed Coalgebraic Partition Refinement
- Efficient Analysis of Cyclic Redundancy Architectures via Boolean Fault Propagation
- Efficient Neural Network Analysis with Sum-of-Infeasibilities
- Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover
- Forest GUMP: A Tool for Explanation
- Formal Verification of the Ethereum 2.0 Beacon Chain
- From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
- GDart: An Ensemble of Tools for Dynamic Symbolic Execution on the Java Virtual Machine (Competition Contribution)
- GWIT: A Witness Validator for Java based on GraalVM (Competition Contribution)
- Graves-CPA: A Graph-Attention Verifier Selector (Competition Contribution)
- HOLL: Program Synthesis for Higher Order Logic Locking
- Inferring Interval-Valued Floating-Point Preconditions
- Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
- Kmclib: Automated Inference and Verification of Session Types from OCaml Programs
- LART: Compiled Abstract Execution - (Competition Contribution)
- Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes
- Learning Realtime One-Counter Automata
- LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions
- MaskD: A Tool for Measuring Masking Fault-Tolerance
- Maximizing Branch Coverage with Constrained Horn Clauses
- Moving Definition Variables in Quantified Boolean Formulas
- NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
- NeuReach: Learning Reachability Functions from Simulations
- On-The-Fly Solving for Symbolic Parity Games
- Practical Applications of the Alternating Cycle Decomposition
- Progress on Software Verification: SV-COMP 2022
- Property Directed Reachability for Generalized Petri Nets
- Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic
- Searching for Ribbon-Shaped Paths in Fair Transition Systems
- Sky Is Not the Limit - Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation
- Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution)
- Symbiotic-Witch: A Klee-Based Violation Witness Checker - (Competition Contribution)
- Synthesis of Compact Strategies for Coordination Programs
- The Complexity of LTL Rational Synthesis
- The Static Analyzer Frama-C in SV-COMP (Competition Contribution)
- The Static Analyzer Infer in SV-COMP (Competition Contribution)
- Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution)
- Transition Power Abstractions for Deep Counterexample Detection
- Ultimate GemCutter and the Axes of Generalization - (Competition Contribution)
- Under-Approximating Expected Total Rewards in POMDPs
- Verified First-Order Monitoring with Recursive Rules
- Verifying Fortran Programs with CIVL
- Wit4Java: A Violation-Witness Validator for Java Verifiers (Competition Contribution)
- ZDD Boolean Synthesis
- cvc5: A Versatile and Industrial-Strength SMT Solver