Venues / CAV /

CAV 2023

67 papers

3D Environment Modeling for Falsification and Beyond with Scenic 3.0 · Eric Vin, Shun Kashiwa, Matthew Rhea, Daniel J. Fremont, Edward Kim, Tommaso Dreossi + 4 more
A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties · Rupak Majumdar, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, Sadegh Soudjani
A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation · S. Akshay, Paul Gastin, R. Govind, Aniruddha R. Joshi, B. Srivathsan
Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization · Masaki Waga
AutoQ: An Automata-Based Quantum Circuit Verifier · Yu-Fang Chen, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai
Automated Analyses of IOT Event Monitoring Systems · Andrew Apicelli, Sam Bayless, Ankush Das, Andrew Gacek, Dhiva Jaganathan, Saswat Padhi + 3 more
Automated Tail Bound Analysis for Probabilistic Recurrence Relations · Yican Sun, Hongfei Fu, Krishnendu Chatterjee, Amir Kafshdar Goharshady
Automated Verification of Correctness for Masked Arithmetic Programs · Mingyang Liu, Fu Song, Taolue Chen
Automatic Program Instrumentation for Automatic Verification · Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer
Bitwuzla · Aina Niemetz, Mathias Preiner
Boolean Abstractions for Realizability Modulo Theories · Andoni Rodríguez, César Sánchez
Bounded Verification for Finite-Field-Blasting - In a Compiler for Zero Knowledge Proofs · Alex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett
Certified Verification for Algebraic Abstraction · Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
Certifying the Fairness of KNN in the Presence of Dataset Bias · Yannan Li, Jingbo Wang, Chao Wang
Closed-Loop Analysis of Vision-Based Autonomous Systems: A Case Study · Corina S. Pasareanu, Ravi Mangal, Divya Gopinath, Sinem Getir Yaman, Calum Imrie, Radu Calinescu + 1 more
Commutativity for Concurrent Program Termination Proofs · Danya Lette, Azadeh Farzan
Complete Multiparty Session Type Projection with Automata · Elaine Li, Felix Stutz, Thomas Wies, Damien Zufferey
Compositional Probabilistic Model Checking with String Diagrams of MDPs · Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo
CoqCryptoLine: A Verified Model Checker with Certified Results · Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang
Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis · S. Akshay, Supratik Chakraborty, Sahil Jain
Decision Procedures for Sequence Theories · Artur Jez, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer
Early Verification of Legal Compliance via Bounded Satisfiability Checking · Nick Feng, Lina Marsso, Mehrdad Sabetzadeh, Marsha Chechik
Efficient Sensitivity Analysis for Parametric Robust Markov Chains · Thom Badings, Sebastian Junges, Ahmadreza Marandi, Ufuk Topcu, Nils Jansen
Exploiting Adjoints in Property Directed Reachability Analysis · Mayuko Kori, Flavio Ascari, Filippo Bonchi, Roberto Bruni, Roberta Gori, Ichiro Hasuo
Fast Approximations of Quantifier Elimination · Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Fast Termination and Workflow Nets · Piotr Hofman, Filip Mazowiecki, Philip Offtermatt
Formally Verified EVM Block-Optimizations · Elvira Albert, Samir Genaim, Daniel Kirchner, Enrique Martin-Martin
Formula Normalizations in Verification · Simon Guilloud, Mario Bucev, Dragana Milovancevic, Viktor Kuncak
Guessing Winning Policies in LTL Synthesis by Semantic Learning · Jan Kretínský, Tobias Meggendorfer, Maximilian Prokop, Sabine Rieder
Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints · Zhengfeng Yang, Li Zhang, Xia Zeng, Xiaochao Tang, Chao Peng, Zhenbing Zeng
Incremental Dead State Detection in Logarithmic Time · Caleb Stanford, Margus Veanes
Kratos2: An SMT-Based Model Checker for Imperative Programs · Alberto Griggio, Martin Jonás
Learning Assumptions for Compositional Verification of Timed Automata · Hanyue Chen, Yu Su, Miaomiao Zhang, Zhiming Liu, Junri Mi
Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM · Nikita Koval, Alexander Fedorov, Maria Sokolova, Dmitry Tsitelov, Dan Alistarh
Local Search for Solving Satisfiability of Polynomial Formulas · Haokun Li, Bican Xia, Tianqi Zhao
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives · S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, Dorde Zikelic
Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms · Eszter Couillard, Philipp Czerner, Javier Esparza, Rupak Majumdar
Model Checking Race-Freedom When "Sequential Consistency for Data-Race-Free Programs" is Guaranteed · Wenhao Wu, Jan Hückelheim, Paul D. Hovland, Ziqing Luo, Stephen F. Siegel
Monitoring Algorithmic Fairness · Thomas A. Henzinger, Mahyar Karimi, Konstantin Kueffner, Kaushik Mallik
NNV 2.0: The Neural Network Verification Tool · Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran, Taylor T. Johnson
Online Causation Monitoring of Signal Temporal Logic · Zhenya Zhang, Jie An, Paolo Arcaini, Ichiro Hasuo
Overcoming Memory Weakness with Unified Fairness - Systematic Verification of Liveness in Weak Memory Models · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankaranarayanan Krishna, Mihir Vahanwala
Ownership Guided C to Rust Translation · Hanliang Zhang, Cristina David, Yijun Yu, Meng Wang
Partial Quantifier Elimination and Property Generation · Eugene Goldberg
Policy Synthesis and Reinforcement Learning for Discounted LTL · Rajeev Alur, Osbert Bastani, Kishor Jothimurugan, Mateo Perez, Fabio Somenzi, Ashutosh Trivedi
Process Equivalence Problems as Energy Games · Benjamin Bisping
QEBVerif: Quantization Error Bound Verification of Neural Networks · Yedi Zhang, Fu Song, Jun Sun
R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software · Chris Johannsen, Phillip H. Jones, Brian Kempa, Kristin Yvonne Rozier, Pei Zhang
Rely-Guarantee Reasoning for Causally Consistent Shared Memory · Ori Lahav, Brijesh Dongol, Heike Wehrheim
Rounding Meets Approximate Model Counting · Jiong Yang, Kuldeep S. Meel
SR-SFLL: Structurally Robust Stripped Functionality Logic Locking · Gourav Takhar, Subhajit Roy
Safe Environmental Envelopes of Discrete Systems · Rômulo Meira-Góes, Ian Dardik, Eunsuk Kang, Stéphane Lafortune, Stavros Tripakis
Satisfiability Modulo Finite Fields · Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark W. Barrett
Search and Explore: Symbiotic Policy Synthesis in POMDPs · Roman Andriushchenko, Alexander Bork, Milan Ceska, Sebastian Junges, Joost-Pieter Katoen, Filip Macák
Searching for i-Good Lemmas to Accelerate Safety Model Checking · Yechuan Xia, Anna Becchi, Alessandro Cimatti, Alberto Griggio, Jianwen Li, Geguang Pu
Second-Order Hyperproperties · Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger
Solving String Constraints Using SAT · Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar + 1 more
Symbolic Quantum Simulation with Quasimodo · Meghana Sistla, Swarat Chaudhuri, Thomas W. Reps
Synthesizing Permissive Winning Strategy Templates for Parity Games · Ashwani Anand, Satya Prakash Nayak, Anne-Kathrin Schmuck
Synthesizing Trajectory Queries from Examples · Stephen Mell, Favyen Bastani, Steve Zdancewic, Osbert Bastani
The Golem Horn Solver · Martin Blicha, Konstantin Britikov, Natasha Sharygina
Unblocking Dynamic Partial Order Reduction · Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
Verifying Generalization in Deep Learning · Guy Amir, Osher Maayan, Tom Zelazny, Guy Katz, Michael Schapira
Verifying the Verifier: eBPF Range Analysis Verification · Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, Santosh Nagarakatte
Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios · Yangge Li, Haoqing Zhu, Katherine Braught, Keyi Shen, Sayan Mitra
nekton: A Linearizability Proof Checker · Roland Meyer, Anton Opaterny, Thomas Wies, Sebastian Wolff
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models · Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, Caroline Trippel