CAV2024: 36TH INTERNATIONAL CONFERENCE ON COMPUTER AIDED VERIFICATION

A
Abate, Alessandro	Bisimulation Learning Stochastic Omega-Regular Verification and Control with Supermartingales
Abdulla, Parosh Aziz	Parsimonious Optimal Dynamic Partial Order Reduction
Abraham, Erika	The Art of SMT Solving
Alt, Leonardo	SolTG: A CHC-based Solidity Test Case Generator
Althoff, Matthias	Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
Amir, Guy	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
An, Jie	Optimization-Based Model Checking for Complex STL Specifications
Ang, Zhendong	Predictive Monitoring with Strong Trace Prefixes
Antonopoulos, Timos	soid: A Tool for Legal Accountability for Automated Decision Making
Arai, Nokiro	How to Solve Math Problems without Talent
Armborst, Lukas	The VerCors Verifier: a Progress Report
Athavale, Anagha	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
Atig, Mohamed Faouzi	Parsimonious Optimal Dynamic Partial Order Reduction
Award, Cav	CAV Award Talk
Azeem, Muqsit	Monitizer: Automating Design and Evaluation of Neural Network Monitors
B
Barrett, Clark	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks Split Gröbner Bases for Satisfiability Modulo Finite Fields
Bartocci, Ezio	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
Basin, David	Proactive Real-Time First-Order Enforcement
Bassa, Alp	Split Gröbner Bases for Satisfiability Modulo Finite Fields
Bassan, Shahaf	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Baumeister, Jan	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Becchi, Anna	Testing the migration from analog to software-based Railway Interlocking Systems
Berger, Martin	LTL learning on GPUs
Bertram, Noah	Verifying Cake Cutting, Faster
Besson, Frédéric	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
Beutner, Raven	Syntax-Guided Automated Program Repair For Hyperproperties
Biere, Armin	CaDiCaL 2.0
Bjørner, Nikolaj	Arithmetic Solving in Z3
Bonakdarpour, Borzoo	Syntax-Guided Automated Program Repair For Hyperproperties
Bonsangue, Marcello	Simulating Quantum Circuits by Model Counting
Bos, Pieter	The VerCors Verifier: a Progress Report
Bosamiya, Jay	(Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Brauße, Franz	SMLP: Symbolic Machine Learning Prover
Britikov, Konstantin	SolTG: A CHC-based Solidity Test Case Generator
Brockman, Mikael	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Bryant, Randal	From Clauses to Klauses
Bu, Lei	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
C
Cai, Shaowei	(Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning
Cano, Filip	soid: A Tool for Legal Accountability for Automated Decision Making
Cao, Jialun	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Chajed, Tej	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Chaudhuri, Swarat	Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
Cheung, Shing-Chi	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Chiari, Michele	SMT-based Symbolic Model-Checking for Operator Precedence Languages
Cho, Chanhee	(Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Christakis, Maria	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
Cimatti, Alessandro	Avoiding the Shoals - A New Approach to Liveness Checking Testing the migration from analog to software-based Railway Interlocking Systems
Cohen, Albert	Strided Difference Bound Matrices
D
D'Antoni, Loris	The SemGuS Toolkit
Daggitt, Matthew	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Dai, Aochu	QReach: A Reachability Analysis Tool for Quantum Markov Chains
Das, Sarbojit	Parsimonious Optimal Dynamic Partial Order Reduction
de Moura, Leonardo	Lean 4: Bridging Formal Mathematics and Software Verification
Dillig, Işıl	Split Gröbner Bases for Satisfiability Modulo Finite Fields Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
Dimitrova, Rayna	Localized Attractor Computations for Infinite-State Games
Ding, Jianqiang	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Dohmen, Taylor	(Distinguished Paper) Regular Reinforcement Learning
Drachsler-Cohen, Dana	Boosting Few-Pixel Robustness Verification via Covering Verification Designs
Dureja, Rohit	Symbolic Model-Checking Intermediate-Language Tool Suite
Dxo,	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
E
Eilers, Marco	Verification Algorithms for Automated Separation Logic Verifiers
Elacqua, Matthew	soid: A Tool for Legal Accountability for Automated Decision Making
F
Faller, Tobias	CaDiCaL 2.0
Fazekas, Katalin	CaDiCaL 2.0
Fedyukovich, Grigory	SolTG: A CHC-based Solidity Test Case Generator
Feldman, Yotam M. Y.	mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
Feng, Yuan	(Recorded) Measurement-based Verification of Quantum Markov Chains
Ferles, Kostas	Split Gröbner Bases for Satisfiability Modulo Finite Fields
Fijalkow, Nathanael	LTL learning on GPUs
Finkbeiner, Bernd	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned Synthesis of Temporal Causality Syntax-Guided Automated Program Repair For Hyperproperties Information Flow guided Synthesis with Unbounded Communication
Fleury, Mathias	CaDiCaL 2.0
Frenkel, Eden	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Frenkel, Hadar	Synthesis of Temporal Causality
Froleyks, Nils	CaDiCaL 2.0
G
Ganesh, Vijay	Opening Remarks
Geatti, Luca	SMT-based Symbolic Model-Checking for Operator Precedence Languages
Giacobbe, Mirco	Bisimulation Learning Stochastic Omega-Regular Verification and Control with Supermartingales
Gigante, Nicola	SMT-based Symbolic Model-Checking for Operator Precedence Languages
Griggio, Alberto	Avoiding the Shoals - A New Approach to Liveness Checking
Grobelna, Marta	Monitizer: Automating Design and Evaluation of Neural Network Monitors
Grosser, Tobias	Strided Difference Bound Matrices
Guan, Ji	(Recorded) Measurement-based Verification of Quantum Markov Chains
Gurfinkel, Arie	Opening Remarks
H
Habermehl, Peter	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Hasuo, Ichiro	Optimization-Based Model Checking for Complex STL Specifications Compositional Value Iteration with Pareto Caching
Havlena, Vojtěch	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
He, Mengda	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Heim, Philippe	Localized Attractor Computations for Infinite-State Games
Heule, Marijn	From Clauses to Klauses
Hečko, Michal	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Hipler, Raik	General Anticipatory Runtime Verification
Holík, Lukáš	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Hsu, Justin	Verifying Cake Cutting, Faster
Hsu, Tzu-Han	Syntax-Guided Automated Program Repair For Hyperproperties
Huang, Pei	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Hublet, François	Proactive Real-Time First-Order Enforcement
Huisman, Marieke	The VerCors Verifier: a Progress Report
I
Irfan, Ahmed	Symbolic Model-Checking Intermediate-Language Tool Suite
Isac, Omri	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
J
Jacobs, Swen	The Reactive Synthesis Competition (SYNTCOMP) Report
Jiang, Hanru	Approximate Relational Reasoning for Quantum Programs
Johannsen, Chris	Symbolic Model-Checking Intermediate-Language Tool Suite
Johnson, Keith J.C.	The SemGuS Toolkit
Jonsson, Bengt	Parsimonious Optimal Dynamic Partial Order Reduction
Judson, Samuel	soid: A Tool for Legal Accountability for Automated Decision Making
Julian, Kyle	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Junges, Sebastian	Compositional Value Iteration with Pareto Caching
K
Kallwies, Hannes	General Anticipatory Runtime Verification
Kanav, Sudeep	Monitizer: Automating Design and Evaluation of Neural Network Monitors
Katz, Guy	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Khasidashvili, Zurab	SMLP: Symbolic Machine Learning Prover
Kincaid, Zachary	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement (Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
Kohn, Florian	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Kokke, Wen	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Komendantskaya, Ekaterina	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Konsta, Alyzia-Maria	What should be observed for optimal reward in POMDPs?
Korovin, Konstantin	SMLP: Symbolic Machine Learning Prover
Kretinsky, Jan	Monitizer: Automating Design and Evaluation of Neural Network Monitors
Krstic, Srdjan	Proactive Real-Time First-Order Enforcement
Könighofer, Bettina	soid: A Tool for Legal Accountability for Automated Decision Making
L
Laarman, Alfons	Simulating Quantum Circuits by Model Counting
Lahav, Ori	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Lai, Tean	Verifying Cake Cutting, Faster
Lengal, Ondrej	Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Lercher, Florian	Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
Leucker, Martin	General Anticipatory Runtime Verification
Li, Haokun	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Li, Jianwen	Avoiding the Shoals - A New Approach to Liveness Checking
Li, Xuandong	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Li, Yixuan	Guiding Enumerative Program Synthesis with Large Language Models
Liang, Zhen	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Lima, Leonardo	Proactive Real-Time First-Order Enforcement
Lin, Fangzhen	On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
Lin, Yi	Dynamic Programming for Symbolic Boolean Realizability and Synthesis
Liu, Jiamou	Lexicographic Ranking Supermartingales with Lazy Lower Bounds
Liu, Si	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Liu, Wenxia	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Lluch Lafuente, Alberto	What should be observed for optimal reward in POMDPs?
Lundfall, Martin	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Luo, Ziqing	Collective Contracts for Message-Passing Parallel Programs
Löhr, Florian	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
M
Maffei, Matteo	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
Manfredi, Guido	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Martinelli Tabajara, Lucas	Dynamic Programming for Symbolic Boolean Realizability and Synthesis
Matheja, Christoph	What should be observed for optimal reward in POMDPs?
Mathur, Umang	Predictive Monitoring with Strong Trace Prefixes
McMillan, Kenneth	Toward Liveness Proofs at Scale
Meel, Kuldeep S.	(Distinguished Paper) Formally Certified Approximate Model Counting
Meggendorfer, Tobias	(Distinguished Paper) (Recorded) Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
Mei, Jingyi	Simulating Quantum Circuits by Model Counting
Metzger, Niklas	Synthesis of Temporal Causality Information Flow guided Synthesis with Unbounded Communication
Miltner, Anders	Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
Mohr, Stefanie	Monitizer: Automating Design and Evaluation of Neural Network Monitors
Moses, Yoram	Information Flow guided Synthesis with Unbounded Communication
Muduli, Sujit	(Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
Murphy, Charlie	Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
Myreen, Magnus O.	(Distinguished Paper) Formally Certified Approximate Model Counting
Müller, Peter	Verification Algorithms for Automated Separation Logic Verifiers
N
Nachmanson, Lev	Arithmetic Solving in Z3
Nayak, Satya Prakash	Localized Attractor Computations for Infinite-State Games
Nickovic, Dejan	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
Niemetz, Aina	Scalable Bit-Blasting with Abstractions
Nukala, Karthik	Symbolic Model-Checking Intermediate-Language Tool Suite
O
Ong, Luke	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Ozdemir, Alex	Split Gröbner Bases for Satisfiability Modulo Finite Fields
P
Padon, Oded	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
Padulkar, Rohan	(Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
Pailoor, Shankara	Split Gröbner Bases for Satisfiability Modulo Finite Fields
Paraskevopoulou, Zoe	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Parno, Bryan	(Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Parsert, Julian	Guiding Enumerative Program Synthesis with Large Language Models
Perez, Mateo	(Distinguished Paper) Regular Reinforcement Learning
Piskac, Ruzica	soid: A Tool for Legal Accountability for Automated Decision Making
Pitchanathan, Arjun	Strided Difference Bound Matrices
Polgreen, Elizabeth	Guiding Enumerative Program Synthesis with Large Language Models
Pollitt, Florian	CaDiCaL 2.0
Pradella, Matteo	SMT-based Symbolic Model-Checking for Operator Precedence Languages
Preiner, Mathias	Scalable Bit-Blasting with Abstractions
Q
Qian, Yuhang	(Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning
Qin, Shengchao	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
R
Reeves, Joseph	From Clauses to Klauses
Refaeli, Idan	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Ren, Dejin	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Reps, Thomas	The SemGuS Toolkit
Reynolds, Andrew	The SemGuS Toolkit
Rieder, Sabine	Monitizer: Automating Design and Evaluation of Neural Network Monitors
Roy, Diptarko	Stochastic Omega-Regular Verification and Control with Supermartingales
Roy, Subhajit	(Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing
Rozier, Kristin Yvonne	Symbolic Model-Checking Intermediate-Language Tool Suite
Rubbens, Robert	The VerCors Verifier: a Progress Report
S
Sagonas, Konstantinos	Parsimonious Optimal Dynamic Partial Order Reduction
Sakar, Ömer	The VerCors Verifier: a Progress Report
Sato, Sota	Optimization-Based Model Checking for Complex STL Specifications
Scaglione, Giuseppe	Testing the migration from analog to software-based Railway Interlocking Systems
Schirmer, Sebastian	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Schmuck, Anne-Kathrin	Localized Attractor Computations for Infinite-State Games
Schnitzer, Yannik	Bisimulation Learning
Schwerhoff, Malte	Verification Algorithms for Automated Separation Logic Verifiers
Seidl, Helmut	The Top-Down Solver Verified: Building Confidence in Static Analyzers
Shabelman, Shahar	Boosting Few-Pixel Robustness Verification via Covering Verification Designs
Shankar, Natarajan	Symbolic Model-Checking Intermediate-Language Tool Suite
Shapira, Yuval	Boosting Few-Pixel Robustness Verification via Covering Verification Designs
Shapiro, Scott	soid: A Tool for Legal Accountability for Automated Decision Making Realizing Leibniz’s Dream
Sharygina, Natasha	SolTG: A CHC-based Solidity Test Case Generator
Shi, Yuhui	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Shoham, Sharon	Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
Siber, Julian	Synthesis of Temporal Causality
Siegel, Stephen F.	Collective Contracts for Message-Passing Parallel Programs
Somenzi, Fabio	(Distinguished Paper) Regular Reinforcement Learning
Soos, Mate	(Distinguished Paper) Formally Certified Approximate Model Counting
Soos, Mate	(Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Stade, Yannick	The Top-Down Solver Verified: Building Confidence in Static Analyzers
Su, Jie	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Sun, Jun	Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors
Sánchez, César	General Anticipatory Runtime Verification
T
Tagomori, Teruhiro	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Takisaka, Toru	Lexicographic Ranking Supermartingales with Lazy Lower Bounds
Talpin, Jean-Pierre	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
Tan, Yong Kiam	(Distinguished Paper) Formally Certified Approximate Model Counting
Tasche, Philip	The VerCors Verifier: a Progress Report
Tian, Cong	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Tilscher, Sarah	The Top-Down Solver Verified: Building Confidence in Static Analyzers
Tinelli, Cesare	Symbolic Model-Checking Intermediate-Language Tool Suite
Torens, Christoph	Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Traytel, Dmitriy	Proactive Real-Time First-Order Enforcement
Trivedi, Ashutosh	(Distinguished Paper) Regular Reinforcement Learning
Turrini, Andrea	(Recorded) Measurement-based Verification of Quantum Markov Chains
V
Valizadeh, Mojtaba	LTL learning on GPUs
van den Haak, Lars	The VerCors Verifier: a Progress Report
van der Vegt, Marck	Compositional Value Iteration with Pareto Caching
Vardi, Moshe Y.	Symbolic Model-Checking Intermediate-Language Tool Suite Dynamic Programming for Symbolic Boolean Realizability and Synthesis
W
Wang, Changjiang	Lexicographic Ranking Supermartingales with Lazy Lower Bounds
Wang, Chenglin	On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
Wang, Jiawan	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Wang, Peixin	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Wang, Yuning	Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
Wang, Ziteng	Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
Watanabe, Kazuki	Compositional Value Iteration with Pareto Caching
Wei, Jiaqi	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Weininger, Maximilian	(Distinguished Paper) (Recorded) Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
Weissenbacher, Georg	(Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence
Wen, Cheng	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Wiesel, Naor	Boosting Few-Pixel Robustness Verification via Covering Verification Designs
Wilcox, James R.	mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
Wu, Chenyu	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Wu, Haoze	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Wu, Min	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Wu, Taoran	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
X
Xia, Yechuan	Avoiding the Shoals - A New Approach to Liveness Checking
Xu, Zhiwu	(Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Xue, Bai	(Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Y
Yan, Peng	Approximate Relational Reasoning for Quantum Programs
Yang, Jiong	(Distinguished Paper) Formally Certified Approximate Model Counting
Ying, Mingsheng	(Recorded) Measurement-based Verification of Quantum Markov Chains
Ying, Mingsheng	QReach: A Reachability Analysis Tool for Quantum Markov Chains
Yu, Nengkun	Approximate Relational Reasoning for Quantum Programs
Yuan, Shenghao	(Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
Z
Zeljić, Aleksandar	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Zhang, Libo	Lexicographic Ranking Supermartingales with Lazy Lower Bounds
Zhang, Min	Marabou 2.0: A Versatile Formal Analyzer of Neural Networks Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Zhang, Muzimiao	(Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Zhang, Ruihan	Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors
Zhang, Yunbo	(Recorded) Probabilistic Access Policies with Automated Reasoning Support
Zhang, Zhenya	Optimization-Based Model Checking for Complex STL Specifications
Zhao, Mengyu	(Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning
Zhi, Dapeng	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Zhou, Yi	(Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Zhu, He	Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
Zhu, Shaowei	(Recorded) Probabilistic Access Policies with Automated Reasoning Support (Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
Zinenko, Oleksandr	Strided Difference Bound Matrices
Zlatkin, Ilia	SolTG: A CHC-based Solidity Test Case Generator
Zohar, Yoni	Scalable Bit-Blasting with Abstractions

Disclaimer | Powered by EasyChair Smart Program