CAV 2020
65 papers
- A Novel Approach for Solving the BMI Problem in Barrier Certificates Generation
- AEON: Attractor Bifurcation Analysis of Parametrised Boolean Networks
- AMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
- Action-Based Model Checking: Logic, Automata, and Reduction
- AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
- An Abstraction-Based Framework for Neural Network Verification
- Approximate Counting of Minimal Unsatisfiable Subsets
- Automata Tutor v3
- Automated and Scalable Verification of Integer Multipliers
- Certifying Certainty and Uncertainty in Approximate Membership Query Structures
- Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
- Code2Inv: A Deep Learning Framework for Program Verification
- Decidable Synthesis of Programs with Uninterpreted Functions
- End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
- Fast and Guaranteed Safe Controller Synthesis for Nonlinear Vehicle Models
- Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI
- Global Guidance for Local Generalization in Model Checking
- Global PAC Bounds for Learning Discrete Time Markov Chains
- Good-Enough Synthesis
- Hampa: Solver-Aided Recency-Aware Replication
- Improved Geometric Path Enumeration for Verifying ReLU Neural Networks
- Interpolation-Based Semantic Gate Extraction and Its Applications to QBF Preprocessing
- Ivy: A Multi-modal Verification Tool for Distributed Algorithms
- Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
- Manthan: A Data-Driven Approach for Boolean Function Synthesis
- Maximum Causal Entropy Specification Inference from Demonstrations
- MetaVal: Witness Validation via Verification
- Must Fault Localization for Program Repair
- NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
- Nonlinear Craig Interpolant Generation
- Optimistic Value Iteration
- PIRK: Scalable Interval Reachability Analysis for High-Dimensional Nonlinear Systems
- PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time
- Parameterized Verification of Systems with Global Synchronization and Guards
- PrIC3: Property Directed Reachability for MDPs
- Program Synthesis Using Deduction-Guided Reinforcement Learning
- Qualitative Controller Synthesis for Consumption Markov Decision Processes
- RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft
- Reachability Analysis Using Message Passing over Tree Decompositions
- Realizing ømega-regular Hyperproperties
- Reasoning over Permissions Regions in Concurrent Separation Logic
- Recursive Data Structures in SPARK
- Refinement for Structured Concurrent Programs
- Root Causing Linearizability Violations
- SAW: A Tool for Safety Analysis of Weakly-Hard Systems
- STMC: Statistical Model Checker with Stratified and Antithetic Sampling
- SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks
- Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
- Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
- Stochastic Games with Lexicographic Reachability-Safety Objectives
- Stratified Abstraction of Access Control Policies
- Symbolic Partial-Order Execution for Testing Multi-Threaded Programs
- Synthesis of Super-Optimized Smart Contracts Using Max-SMT
- Synthesizing JIT Compilers for In-Kernel DSLs
- Systematic Generation of Diverse Benchmarks for DNN Verification
- TarTar: A Timed Automata Repair Tool
- The Move Prover
- Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling
- Towards Model Checking Real-World Software-Defined Networks
- Unbounded-Time Safety Verification of Stochastic Differential Dynamics
- Validation of Abstract Side-Channel Models for Computer Architectures
- Verification of Deep Convolutional Neural Networks Using ImageStars
- Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
- Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
- fault: A Python Embedded Domain-Specific Language for Metaprogramming Portable Hardware Verification Components