researchr
explore
Tags
Journals
Conferences
Authors
Profiles
Groups
calendar
New Conferences
Events
Deadlines
search
search
You are not signed in
Sign in
Sign up
Links
Filter by Year
[-]
OR
AND
NOT
1
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016
2017
2018
2019
2020
2021
2022
2023
Filter by Tag
[+]
OR
AND
NOT
1
algebra
C++
Meta-Environment
abstraction
analysis
composition
constraints
data-flow
design
e-science
logic
meta-model
meta-objects
model checking
program verification
protocol
refinement
rule-based
systematic-approach
testing
Filter by Author
[+]
OR
AND
NOT
1
Ahmed Bouajjani
Alessandro Cimatti
Amir Pnueli
Bernd Finkbeiner
Byron Cook
Clark W. Barrett
Daniel Kroening
David L. Dill
Edmund M. Clarke
Joost-Pieter Katoen
Kenneth L. McMillan
Krishnendu Chatterjee
Moshe Y. Vardi
Orna Grumberg
Rajeev Alur
Rupak Majumdar
Sanjit A. Seshia
Shaz Qadeer
Thomas A. Henzinger
Thomas W. Reps
Filter by Top terms
[+]
OR
AND
NOT
1
abstraction
analysis
automata
automatic
checking
efficient
formal
hybrid
logic
model
programs
state
symbolic
synthesis
systems
time
tool
using
verification
verifying
CAV (cav)
Editions
Publications
Viewing Publication 1 - 100 from 1983
2023
A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation
S. Akshay 0001
,
Paul Gastin
,
R. Govind 0001
,
Aniruddha R. Joshi
,
B. Srivathsan
.
cav 2023
:
266-288
[doi]
nekton: A Linearizability Proof Checker
Roland Meyer 0001
,
Anton Opaterny
,
Thomas Wies
,
Sebastian Wolff 0001
.
cav 2023
:
170-183
[doi]
Counterexample Guided Knowledge Compilation for Boolean Functional Synthesis
S. Akshay 0001
,
Supratik Chakraborty
,
Sahil Jain
.
cav 2023
:
367-389
[doi]
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
S. Akshay 0001
,
Krishnendu Chatterjee
,
Tobias Meggendorfer
,
Dorde Zikelic
.
cav 2023
:
86-112
[doi]
CoqCryptoLine: A Verified Model Checker with Certified Results
Ming-Hsien Tsai 0001
,
Yu-Fu Fu
,
Jiaxiang Liu 0001
,
Xiaomu Shi
,
Bow-Yaw Wang
,
Bo-Yin Yang
.
cav 2023
:
227-240
[doi]
Certified Verification for Algebraic Abstraction
Ming-Hsien Tsai 0001
,
Yu-Fu Fu
,
Jiaxiang Liu 0001
,
Xiaomu Shi
,
Bow-Yaw Wang
,
Bo-Yin Yang
.
cav 2023
:
329-349
[doi]
AutoQ: An Automata-Based Quantum Circuit Verifier
Yu-Fang Chen 0001
,
Kai-Min Chung
,
Ondrej Lengál
,
Jyun-Ao Lin
,
Wei-Lun Tsai
.
cav 2023
:
139-153
[doi]
Rounding Meets Approximate Model Counting
Jiong Yang 0002
,
Kuldeep S. Meel
.
cav 2023
:
132-162
[doi]
Compositional Probabilistic Model Checking with String Diagrams of MDPs
Kazuki Watanabe 0003
,
Clovis Eberhart
,
Kazuyuki Asada
,
Ichiro Hasuo
.
cav 2023
:
40-61
[doi]
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
.
cav 2023
:
184-205
[doi]
Formally Verified EVM Block-Optimizations
Elvira Albert
,
Samir Genaim
,
Daniel Kirchner
,
Enrique Martin-Martin
.
cav 2023
:
176-189
[doi]
Policy Synthesis and Reinforcement Learning for Discounted LTL
Rajeev Alur
,
Osbert Bastani
,
Kishor Jothimurugan
,
Mateo Perez
,
Fabio Somenzi
,
Ashutosh Trivedi 0001
.
cav 2023
:
415-435
[doi]
Automatic Program Instrumentation for Automatic Verification
Jesper Amilon
,
Zafer Esen
,
Dilian Gurov
,
Christian Lidström
,
Philipp Rümmer
.
cav 2023
:
281-304
[doi]
Verifying Generalization in Deep Learning
Guy Amir
,
Osher Maayan
,
Tom Zelazny
,
Guy Katz
,
Michael Schapira
.
cav 2023
:
438-455
[doi]
Synthesizing Permissive Winning Strategy Templates for Parity Games
Ashwani Anand
,
Satya Prakash Nayak
,
Anne-Kathrin Schmuck
.
cav 2023
:
436-458
[doi]
Search and Explore: Symbiotic Policy Synthesis in POMDPs
Roman Andriushchenko
,
Alexander Bork
,
Milan Ceska 0002
,
Sebastian Junges
,
Joost-Pieter Katoen
,
Filip Macák
.
cav 2023
:
113-135
[doi]
Automated Analyses of IOT Event Monitoring Systems
Andrew Apicelli
,
Sam Bayless
,
Ankush Das
,
Andrew Gacek
,
Dhiva Jaganathan
,
Saswat Padhi
,
Vaibhav Sharma 0001
,
Michael W. Whalen
,
Raveesh Yadav
.
cav 2023
:
27-39
[doi]
Efficient Sensitivity Analysis for Parametric Robust Markov Chains
Thom S. Badings
,
Sebastian Junges
,
Ahmadreza Marandi
,
Ufuk Topcu
,
Nils Jansen 0001
.
cav 2023
:
62-85
[doi]
Second-Order Hyperproperties
Raven Beutner
,
Bernd Finkbeiner
,
Hadar Frenkel
,
Niklas Metzger 0001
.
cav 2023
:
309-332
[doi]
Process Equivalence Problems as Energy Games
Benjamin Bisping
.
cav 2023
:
85-106
[doi]
The Golem Horn Solver
Martin Blicha
,
Konstantin Britikov
,
Natasha Sharygina
.
cav 2023
:
209-223
[doi]
Learning Assumptions for Compositional Verification of Timed Automata
Hanyue Chen
,
Yu Su
,
Miaomiao Zhang
,
Zhiming Liu
,
Junri Mi
.
cav 2023
:
40-61
[doi]
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
Matthias Cosler
,
Christopher Hahn
,
Daniel Mendoza
,
Frederik Schmitt
,
Caroline Trippel
.
cav 2023
:
383-396
[doi]
Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms
Eszter Couillard
,
Philipp Czerner
,
Javier Esparza
,
Rupak Majumdar
.
cav 2023
:
437-458
[doi]
Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II
Constantin Enea
,
Akash Lal
, editors,
Volume 13965 of
Lecture Notes in Computer Science
, Springer,
2023.
[doi]
Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III
Constantin Enea
,
Akash Lal
, editors,
Volume 13966 of
Lecture Notes in Computer Science
, Springer,
2023.
[doi]
Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I
Constantin Enea
,
Akash Lal
, editors,
Volume 13964 of
Lecture Notes in Computer Science
, Springer,
2023.
[doi]
Early Verification of Legal Compliance via Bounded Satisfiability Checking
Nick Feng
,
Lina Marsso
,
Mehrdad Sabetzadeh
,
Marsha Chechik
.
cav 2023
:
374-396
[doi]
Fast Approximations of Quantifier Elimination
Isabel Garcia-Contreras
,
Hari Govind V. K.
,
Sharon Shoham
,
Arie Gurfinkel
.
cav 2023
:
64-86
[doi]
Partial Quantifier Elimination and Property Generation
Eugene Goldberg
.
cav 2023
:
110-131
[doi]
Kratos2: An SMT-Based Model Checker for Imperative Programs
Alberto Griggio
,
Martin Jonás
.
cav 2023
:
423-436
[doi]
Formula Normalizations in Verification
Simon Guilloud
,
Mario Bucev
,
Dragana Milovancevic
,
Viktor Kuncak
.
cav 2023
:
398-422
[doi]
Monitoring Algorithmic Fairness
Thomas A. Henzinger
,
Mahyar Karimi
,
Konstantin Kueffner
,
Kaushik Mallik
.
cav 2023
:
358-382
[doi]
Fast Termination and Workflow Nets
Piotr Hofman
,
Filip Mazowiecki
,
Philip Offtermatt
.
cav 2023
:
132-155
[doi]
Decision Procedures for Sequence Theories
Artur Jez
,
Anthony W. Lin
,
Oliver Markgraf
,
Philipp Rümmer
.
cav 2023
:
18-40
[doi]
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 0009
.
cav 2023
:
483-497
[doi]
Unblocking Dynamic Partial Order Reduction
Michalis Kokologiannakis
,
Iason Marmanis
,
Viktor Vafeiadis
.
cav 2023
:
230-250
[doi]
Exploiting Adjoints in Property Directed Reachability Analysis
Mayuko Kori
,
Flavio Ascari
,
Filippo Bonchi
,
Roberto Bruni
,
Roberta Gori
,
Ichiro Hasuo
.
cav 2023
:
41-63
[doi]
Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM
Nikita Koval
,
Alexander Fedorov
,
Maria Sokolova
,
Dmitry Tsitelov
,
Dan Alistarh
.
cav 2023
:
156-169
[doi]
Guessing Winning Policies in LTL Synthesis by Semantic Learning
Jan Kretínský
,
Tobias Meggendorfer
,
Maximilian Prokop
,
Sabine Rieder
.
cav 2023
:
390-414
[doi]
Rely-Guarantee Reasoning for Causally Consistent Shared Memory
Ori Lahav
,
Brijesh Dongol
,
Heike Wehrheim
.
cav 2023
:
206-229
[doi]
Commutativity for Concurrent Program Termination Proofs
Danya Lette
,
Azadeh Farzan
.
cav 2023
:
109-131
[doi]
Complete Multiparty Session Type Projection with Automata
Elaine Li
,
Felix Stutz
,
Thomas Wies
,
Damien Zufferey
.
cav 2023
:
350-373
[doi]
Verse: A Python Library for Reasoning About Multi-agent Hybrid System Scenarios
Yangge Li
,
Haoqing Zhu
,
Katherine Braught
,
Keyi Shen
,
Sayan Mitra
.
cav 2023
:
351-364
[doi]
Local Search for Solving Satisfiability of Polynomial Formulas
Haokun Li
,
Bican Xia
,
Tianqi Zhao
.
cav 2023
:
87-109
[doi]
Certifying the Fairness of KNN in the Presence of Dataset Bias
Yannan Li
,
Jingbo Wang
,
Chao Wang
.
cav 2023
:
335-357
[doi]
Automated Verification of Correctness for Masked Arithmetic Programs
Mingyang Liu
,
Fu Song
,
Taolue Chen
.
cav 2023
:
255-280
[doi]
NNV 2.0: The Neural Network Verification Tool
Diego Manzanas Lopez
,
Sung Woo Choi
,
Hoang-Dung Tran
,
Taylor T. Johnson
.
cav 2023
:
397-412
[doi]
Solving String Constraints Using SAT
Kevin Lotz
,
Amit Goel
,
Bruno Dutertre
,
Benjamin Kiesl-Reiter
,
Soonho Kong
,
Rupak Majumdar
,
Dirk Nowotka
.
cav 2023
:
187-208
[doi]
A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties
Rupak Majumdar
,
Kaushik Mallik
,
Mateusz Rychlicki
,
Anne-Kathrin Schmuck
,
Sadegh Soudjani
.
cav 2023
:
3-15
[doi]
Safe Environmental Envelopes of Discrete Systems
Rômulo Meira-Góes
,
Ian Dardik
,
Eunsuk Kang
,
Stéphane Lafortune
,
Stavros Tripakis
.
cav 2023
:
326-350
[doi]
Synthesizing Trajectory Queries from Examples
Stephen Mell
,
Favyen Bastani
,
Steve Zdancewic
,
Osbert Bastani
.
cav 2023
:
459-484
[doi]
Bitwuzla
Aina Niemetz
,
Mathias Preiner
.
cav 2023
:
3-17
[doi]
Bounded Verification for Finite-Field-Blasting - In a Compiler for Zero Knowledge Proofs
Alex Ozdemir
,
Riad S. Wahby
,
Fraser Brown
,
Clark W. Barrett
.
cav 2023
:
154-175
[doi]
Satisfiability Modulo Finite Fields
Alex Ozdemir
,
Gereon Kremer
,
Cesare Tinelli
,
Clark W. Barrett
.
cav 2023
:
163-186
[doi]
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
,
Huafeng Yu
.
cav 2023
:
289-303
[doi]
Boolean Abstractions for Realizability Modulo Theories
Andoni Rodríguez
,
César Sánchez 0001
.
cav 2023
:
305-328
[doi]
Symbolic Quantum Simulation with Quasimodo
Meghana Sistla
,
Swarat Chaudhuri
,
Thomas W. Reps
.
cav 2023
:
213-225
[doi]
Incremental Dead State Detection in Logarithmic Time
Caleb Stanford
,
Margus Veanes
.
cav 2023
:
241-264
[doi]
Automated Tail Bound Analysis for Probabilistic Recurrence Relations
Yican Sun
,
Hongfei Fu 0001
,
Krishnendu Chatterjee
,
Amir Kafshdar Goharshady
.
cav 2023
:
16-39
[doi]
SR-SFLL: Structurally Robust Stripped Functionality Logic Locking
Gourav Takhar
,
Subhajit Roy 0001
.
cav 2023
:
190-212
[doi]
3D Environment Modeling for Falsification and Beyond with Scenic 3.0
Eric Vin
,
Shun Kashiwa
,
Matthew Rhea
,
Daniel J. Fremont
,
Edward Kim
,
Tommaso Dreossi
,
Shromona Ghosh
,
Xiangyu Yue
,
Alberto L. Sangiovanni-Vincentelli
,
Sanjit A. Seshia
.
cav 2023
:
253-265
[doi]
Verifying the Verifier: eBPF Range Analysis Verification
Harishankar Vishwanathan
,
Matan Shachnai
,
Srinivas Narayana
,
Santosh Nagarakatte
.
cav 2023
:
226-251
[doi]
Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization
Masaki Waga
.
cav 2023
:
3-26
[doi]
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
.
cav 2023
:
265-287
[doi]
Searching for i-Good Lemmas to Accelerate Safety Model Checking
Yechuan Xia
,
Anna Becchi
,
Alessandro Cimatti
,
Alberto Griggio
,
Jianwen Li
,
Geguang Pu
.
cav 2023
:
288-308
[doi]
Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-Avoid Constraints
Zhengfeng Yang
,
Li Zhang
,
Xia Zeng
,
Xiaochao Tang
,
Chao Peng 0004
,
Zhenbing Zeng
.
cav 2023
:
304-325
[doi]
Online Causation Monitoring of Signal Temporal Logic
Zhenya Zhang
,
Jie An 0001
,
Paolo Arcaini
,
Ichiro Hasuo
.
cav 2023
:
62-84
[doi]
QEBVerif: Quantization Error Bound Verification of Neural Networks
Yedi Zhang
,
Fu Song
,
Jun Sun 0001
.
cav 2023
:
413-437
[doi]
Ownership Guided C to Rust Translation
Hanliang Zhang
,
Cristina David
,
Yijun Yu
,
Meng Wang
.
cav 2023
:
459-482
[doi]
2022
Front Matter, Table of Contents, Preface, Conference Organization
cav 2022
:
[doi]
Distilling Constraints in Zero-Knowledge Protocols
Elvira Albert
,
Marta Bellés-Muñoz
,
Miguel Isabel
,
Clara Rodríguez-Núñez
,
Albert Rubio
.
cav 2022
:
430-443
[doi]
SolCMC: Solidity Compiler's Model Checker
Leonardo Alt
,
Martin Blicha
,
Antti E. J. Hyvärinen
,
Natasha Sharygina
.
cav 2022
:
325-338
[doi]
Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
Stanley Bak
,
Sergiy Bogomolov
,
Brandon Hencey
,
Niklas Kochdumper
,
Ethan Lew
,
Kostiantyn Potomkin
.
cav 2022
:
490-510
[doi]
Automatic Generation of Attacker Contracts in Solidity
Ignacio Ballesteros
,
Clara Benac Earle
,
Luis Eduardo Bueso de Barrio
,
Lars-Åke Fredlund
,
Ángel Herranz
,
Julio Mariño
.
cav 2022
:
[doi]
Data-Driven Invariant Learning for Probabilistic Programs
Jialu Bao
,
Nitesh Trivedi
,
Drashti Pathak
,
Justin Hsu
,
Subhajit Roy
.
cav 2022
:
33-54
[doi]
MEV-Freedom, in DeFi and Beyond (Invited Talk)
Massimo Bartoletti
.
cav 2022
:
[doi]
Software Verification of Hyperproperties Beyond k-Safety
Raven Beutner
,
Bernd Finkbeiner
.
cav 2022
:
341-362
[doi]
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
Ahmed Bouajjani
,
Wael-Amine Boutglay
,
Peter Habermehl
.
cav 2022
:
282-303
[doi]
Proofgold: Blockchain for Formal Methods
Chad E. Brown
,
Cezary Kaliszyk
,
Thibault Gauthier
,
Josef Urban
.
cav 2022
:
[doi]
Playing Against Fair Adversaries in Stochastic Games with Total Rewards
Pablo F. Castro
,
Pedro R. D'Argenio
,
Ramiro Demasi
,
Luciano Putruele
.
cav 2022
:
48-69
[doi]
Multi: A Formal Playground for Multi-Smart Contract Interaction
Martín Ceresa
,
César Sánchez
.
cav 2022
:
[doi]
Verified Erasure Correction in Coq with MathComp and VST
Joshua M. Cohen
,
Qinshi Wang
,
Andrew W. Appel
.
cav 2022
:
272-292
[doi]
4th International Workshop on Formal Methods for Blockchains, FMBC@CAV 2022, August 11, 2022, Haifa, Israel
Zaynah Dargaye
,
Clara Schneidewind
, editors,
Volume 105 of
OASIcs
, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2022.
[doi]
Synthesis and Analysis of Petri Nets from Causal Specifications
Mateus de Oliveira Oliveira
.
cav 2022
:
447-467
[doi]
Neural Networks in Imandra: Matrix Representation as a Verification Choice
Remi Desmartin
,
Grant O. Passmore
,
Ekaterina Komendentskaya
.
cav 2022
:
78-95
[doi]
FORQ-Based Language Inclusion Formal Testing
Kyveli Doveri
,
Pierre Ganty
,
Nicolas Mazzocchi
.
cav 2022
:
109-129
[doi]
Reasoning About Data Trees Using CHCs
Marco Faella
,
Gennaro Parlato
.
cav 2022
:
249-271
[doi]
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
Andreas Gittis
,
Eric Vin
,
Daniel J. Fremont
.
cav 2022
:
526-546
[doi]
RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
Eric Goubault
,
Sylvie Putot
.
cav 2022
:
511-523
[doi]
MoGym: Using Formal Models for Training and Verifying Decision-making Agents
Timo P. Gros
,
Holger Hermanns
,
Jörg Hoffmann 0001
,
Michaela Klauck
,
Maximilian A. Köhl
,
Verena Wolf
.
cav 2022
:
430-443
[doi]
Complementing Büchi Automata with Ranker
Vojtech Havlena
,
Ondrej Lengál
,
Barbora Smahlíková
.
cav 2022
:
188-201
[doi]
Capture, Analyze, Diagnose: Realizability Checking Of Requirements in FRET
Andreas Katis
,
Anastasia Mavridou
,
Dimitra Giannakopoulou
,
Thomas Pressburger
,
Johann Schumann
.
cav 2022
:
490-504
[doi]
Verified Numerical Methods for Ordinary Differential Equations
Ariel E. Kellison
,
Andrew W. Appel
.
cav 2022
:
147-163
[doi]
A Cascade of Checkers for Run-time Certification of Local Robustness
Ravi Mangal
,
Corina S. Pasareanu
.
cav 2022
:
15-28
[doi]
Example Guided Synthesis of Linear Approximations for Neural Network Verification
Brandon Paulsen
,
Chao Wang 0001
.
cav 2022
:
149-170
[doi]
Minimal Multi-Layer Modifications of Deep Neural Networks
Idan Refaeli
,
Guy Katz
.
cav 2022
:
46-66
[doi]
A Billion SMT Queries a Day (Invited Paper)
Neha Rungta
.
cav 2022
:
3-18
[doi]
Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II
Sharon Shoham
,
Yakir Vizel
, editors,
Volume 13372 of
Lecture Notes in Computer Science
, Springer,
2022.
[doi]
Differentiable Logics for Neural Network Training and Verification
Natalia Slusarz
,
Ekaterina Komendantskaya
,
Matthew L. Daggitt
,
Robert J. Stewart 0001
.
cav 2022
:
67-77
[doi]
Sign in
or
sign up
to see more results.