Editors: Yakir Vizel, Sharon Shoham and Hari Govind Vediramana Krishnan

Neha RungtaA Billion SMT Queries a Day
Arie GurfinkelProgram Verification with Constrained Horn Clauses (Invited Paper)
Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu and Subhajit RoyData-Driven Invariant Learning for Probabilistic ProgramsAug 07 09:00
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer and Đorđe ŽikelićSound and Complete Certificates for Quantitative Termination Analysis of Probabilistic ProgramsAug 07 09:20
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias WinklerDoes a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating FunctionsAug 07 09:40
Sebastian Junges and Matthijs T. J. SpaanAbstraction-Refinement for Hierarchical Probabilistic ModelsAug 07 10:00
Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh and Martin VechevShared Certificates for Neural Network VerificationAug 07 14:00
Brandon Paulsen and Chao WangExample Guided Synthesis of Linear Approximations for Neural Network VerificationAug 07 14:20
Long H. Pham and Jun SunVerifying Neural Networks Against Backdoor AttacksAug 07 14:40
Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen and Min ZhangTrainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement LearningAug 07 15:00
Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir and Idan RefaeliNeural Network Robustness as a Verification Property: A Principled Case StudyAug 07 15:20
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga and Ichiro HasuoThe Lattice-Theoretic Essence of Property Directed Reachability AnalysisAug 07 16:00
Yucheng Ji, Hongfei Fu, Bin Fang and Haibo ChenAffine Loop Invariant Generation via Matrix AlgebraAug 07 16:20
Ahmed Bouajjani, Wael-Amine Boutglay and Peter HabermehlData-driven Numerical Invariant Synthesis with Automatic Generation of AttributesAug 07 16:40
Prantik Chatterjee, Jaydeepsinh Meda, Akash Lal and Subhajit RoyProof-guided Underapproximation Widening for Bounded Model CheckingAug 07 17:00
Leonardo Alt, Martin Blicha, Antti Hyvärinen and Natasha SharyginaSolCMC: Solidity Compiler’s Model CheckerAug 07 17:20
Raven Beutner and Bernd FinkbeinerSoftware Verification of Hyperproperties Beyond k-SafetyAug 08 09:00
Priyanka Golia, Brendan Juba and Kuldeep S. MeelA Scalable Shannon Entropy EstimatorAug 08 09:20
Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang and Wanwei LiuPoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party ComputationAug 08 09:40
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger and Julian SiberExplaining Hyperproperty ViolationsAug 08 10:00
Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez and Albert RubioDistilling Constraints in Zero-Knowledge ProtocolsAug 08 10:20
Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga and Kohei SuenagaOblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic EncryptionAug 08 14:00
Anna Becchi and Alessandro CimattiAbstraction Modulo Stability for Reverse EngineeringAug 08 14:20
Stanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, Ethan Lew and Kostiantyn PotomkinReachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope RefinementAug 08 14:40
Eric Goubault and Sylvie PutotRINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled SystemsAug 08 15:00
Geunyeol Yu, Jia Lee and Kyungmin BaeSTLmc: Robust STL Model Checking of Hybrid Systems using SMTAug 08 15:10
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. SeshiaUCLID5: Multi-Modal Formal Modeling, Verification, and SynthesisAug 08 15:20
Chaitanya Agarwal, Shibashis Guha, Jan Křetínský and Pazhamalai MuruganandhamPAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDPAug 08 16:00
Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga and Matthias VolkSampling-Based Verification of CTMCs with Uncertain RatesAug 08 16:20
Pablo Castro, Pedro R. D'Argenio, Luciano Putruele and Ramiro DemasiPlaying Against Fair Adversaries in Stochastic Games with Total RewardsAug 08 16:40
Lorenz Leutgeb, Georg Moser and Florian ZulegerAutomated Expected Amortised Cost Analysis of Probabilistic Data StructuresAug 08 17:00
Aina Niemetz, Mathias Preiner and Clark BarrettMurxla: A Modular and Highly Extensible API Fuzzer for SMT SolversAug 08 17:20
Kyveli Doveri, Pierre Ganty and Nicolas MazzocchiFORQ-based Language Inclusion Formal TestingAug 09 11:00
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller and Alexander J. SummersSound Automation of Magic WandsAug 09 11:20
Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi and Lijun ZhangDivide-and-Conquer Determinization of Büchi Automata based on SCC DecompositionAug 09 11:40
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard and Henrich LaukoFrom Spot 2.0 to Spot 2.10: What's New?Aug 09 12:00
Vojtěch Havlena, Ondrej Lengal and Barbora ŠmahlíkováComplementing Büchi Automata with RankerAug 09 12:10
Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare TinelliEven Faster Conflicts and Lazier Reductions for String SolversAug 09 14:00
Shaowei Cai, Bohan Li and Xindi ZhangLocal Search For SMT on Linear Integer ArithmeticAug 09 14:20
Marco Faella and Gennaro ParlatoReasoning about Data Trees using CHCsAug 09 14:40
Joshua M. Cohen, Qinshi Wang and Andrew W. AppelVerified Erasure Correction in Coq with MathComp and VSTAug 09 15:00
Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg and Emmanuel BaccelliEnd-to-end Mechanised Proof of an eBPF Virtual Machine for MicrocontrollersAug 09 15:20
Joonwon Choi, Adam Chlipala and ArvindHemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence ProtocolsAug 09 15:40
Kishor Jothimurugan, Suguman Bansal, Osbert Bastani and Rajeev AlurSpecification-Guided Learning of Nash Equilibria with High Social WelfareAug 10 14:00
Jingbo Wang, Yannan Li and Chao WangSynthesizing Fair Decision Trees via Iterative Constraint SolvingAug 10 14:20
Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo and Juneyoung LeeSMT-based Translation Validation for Machine Learning CompilerAug 10 14:40
Ji Guan, Wang Fang and Mingsheng YingVerifying Fairness in Quantum Machine LearningAug 10 15:00
Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Maximilian Alexander Köhl and Verena WolfMoGym: Using Formal Models for Training and Verifying Decision-making AgentsAug 10 15:20
Mateus De Oliveira OliveiraSynthesis and Analysis of Petri Nets from Causal SpecificationsAug 10 16:00
Michael Blondin, Filip Mazowiecki and Philip OfftermattVerifying generalised and structural soundness of workflow nets via relaxationsAug 10 16:20
Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger and Johann SchumannCapture, Analyze, Diagnose: Realizability Checking of Requirements in FRETAug 10 16:40
Bernd Finkbeiner, Niklas Metzger and Yoram MosesInformation Flow Guided SynthesisAug 10 16:50
Andreas Gittis, Eric Vin and Daniel FremontRandomized Synthesis for Diversity and Cost Constraints with Control ImprovisationAug 10 17:10