CAV 2022
53 papers
- A Billion SMT Queries a Day (Invited Paper)
- A Scalable Shannon Entropy Estimator
- Abstraction Modulo Stability for Reverse Engineering
- Abstraction-Refinement for Hierarchical Probabilistic Models
- Affine Loop Invariant Generation via Matrix Algebra
- Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
- Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET
- Complementing Büchi Automata with Ranker
- Data-Driven Invariant Learning for Probabilistic Programs
- Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
- Distilling Constraints in Zero-Knowledge Protocols
- Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition
- Does a Program Yield the Right Distribution? - Verifying Probabilistic Programs via Generating Functions
- End-to-End Mechanized Proof of an eBPF Virtual Machine for Micro-controllers
- Even Faster Conflicts and Lazier Reductions for String Solvers
- Example Guided Synthesis of Linear Approximations for Neural Network Verification
- Explaining Hyperproperty Violations
- FORQ-Based Language Inclusion Formal Testing
- From Spot 2.0 to Spot 2.10: What's New?
- Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
- Information Flow Guided Synthesis
- Local Search for SMT on Linear Integer Arithmetic
- MoGym: Using Formal Models for Training and Verifying Decision-making Agents
- Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
- Neural Network Robustness as a Verification Property: A Principled Case Study
- Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
- PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
- Playing Against Fair Adversaries in Stochastic Games with Total Rewards
- PoS4MPC: Automated Security Policy Synthesis for Secure Multi-party Computation
- Program Verification with Constrained Horn Clauses (Invited Paper)
- Proof-Guided Underapproximation Widening for Bounded Model Checking
- RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
- Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
- Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
- Reasoning About Data Trees Using CHCs
- SMT-Based Translation Validation for Machine Learning Compiler
- STLmc: Robust STL Model Checking of Hybrid Systems Using SMT
- Sampling-Based Verification of CTMCs with Uncertain Rates
- Shared Certificates for Neural Network Verification
- Software Verification of Hyperproperties Beyond k-Safety
- SolCMC: Solidity Compiler's Model Checker
- Sound Automation of Magic Wands
- Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
- Specification-Guided Learning of Nash Equilibria with High Social Welfare
- Synthesis and Analysis of Petri Nets from Causal Specifications
- Synthesizing Fair Decision Trees via Iterative Constraint Solving
- The Lattice-Theoretic Essence of Property Directed Reachability Analysis
- Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning
- UCLID5: Multi-modal Formal Modeling, Verification, and Synthesis
- Verified Erasure Correction in Coq with MathComp and VST
- Verifying Fairness in Quantum Machine Learning
- Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations
- Verifying Neural Networks Against Backdoor Attacks