Venues / TACAS /

TACAS 2024

70 papers

A Comprehensive Specification and Verification of the L4 Microkernel API · Leping Zhang, Yongwang Zhao, Jianxin Li
A Logical Treatment of Finite Automata · Nishant Rodrigues, Mircea Sebe, Xiaohong Chen, Grigore Rosu
A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Teleportation · Shang-Wei Lin, Tzu-Fan Wang, Yean-Ru Chen, Zhe Hou, David Sanán, Yon Shin Teo
A State-of-the-Art Karp-Miller Algorithm Certified in Coq · Thibault Hilaire, David Ilcinkas, Jérôme Leroux
AISE: A Symbolic Verifier by Synergizing Abstract Interpretation and Symbolic Execution (Competition Contribution) · Zhen Wang, Zhenbang Chen
Accelerated Bounded Model Checking Using Interpolation Based Summaries · Mayank Solanki, Prantik Chatterjee, Akash Lal, Subhajit Roy
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains · Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler
Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains · Lukas Westhofen, Christian Neurohr, Jean Christoph Jung, Daniel Neider
Asynchronous Subtyping by Trace Relaxation · Laura Bocchi, Andy King, Maurizio Murgia
Auction-Based Scheduling · Guy Avni, Kaushik Mallik, Suman Sadhukhan
Automate where Automation Fails: Proof Strategies for Frama-C/WP · Loïc Correnson, Allan Blanchard, Adel Djoudi, Nikolai Kosmatov
Automated Software Verification of Hyperliveness · Raven Beutner
Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers · Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee, Nils Sirrenberg
Bubaak-SpLit: Split what you cannot verify (Competition contribution) · Marek Chalupa, Cedric Richter
CESAR: Control Envelope Synthesis via Angelic Refinements · Aditi Kabra, Jonathan Laurent, Stefan Mitsch, André Platzer
CPAchecker 2.3 with Strategy Selection - (Competition Contribution) · Daniel Baier, Dirk Beyer, Po-Chun Chien, Marek Jankola, Matthias Kettl, Nian-Ze Lee + 5 more
CPV: A Circuit-Based Program Verifier · Po-Chun Chien, Nian-Ze Lee
CTMCs with Imprecisely Timed Observations · Thom Badings, Matthias Volk, Sebastian Junges, Mariëlle Stoelinga, Nils Jansen
ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution) · Levente Bajczi, Zsófia Ádám, Zoltán Micskei
DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories · Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Mike Whalen + 2 more
Decidable Verification under Localized Release-Acquire Concurrency · Abhishek Kr Singh, Ori Lahav
Deciding Boolean Separation Logic via Small Models · Tomás Dacík, Adam Rogalewicz, Tomás Vojnar, Florian Zuleger
Dissipative quadratizations of polynomial ODE systems · Yubo Cai, Gleb Pogudin
ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution) · Rafael Sá Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov + 6 more
EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution) · Levente Bajczi, Dániel Szekeres, Milán Mondok, Zsófia Ádám, Márk Somorjai, Csanád Telbisz + 2 more
Enhancing GenMC's Usability and Performance · Michalis Kokologiannakis, Rupak Majumdar, Viktor Vafeiadis
Explainable Online Monitoring of Metric First-Order Temporal Logic · Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel
Fast Symbolic Computation of Bottom SCCs · Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jørgensen, Jaco van de Pol, Andreas Pavlogiannis
Formally Verifying an Efficient Sorter · Bernhard Beckert, Peter Sanders, Mattias Ulbrich, Julian Wiesler, Sascha Witt
Formally verified asymptotic consensus in robust networks · Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin, Manos Kapritsos, Dimitra Panagou
Forward and Backward Constrained Bisimulations for Quantum Circuits · Antonio Jiménez-Pastor, Kim G. Larsen, Mirco Tribastone, Max Tschaikowski
Fully Generalized Reactivity(1) Synthesis · Rüdiger Ehlers, Ayrat Khalimov
Goblint Validator: Correctness Witness Validation by Abstract Interpretation - (Competition Contribution) · Simmo Saan, Julian Erhard, Michael Schwarz, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher + 2 more
Goblint: Abstract Interpretation for Memory Safety and Termination - (Competition Contribution) · Simmo Saan, Julian Erhard, Michael Schwarz, Stanimir Bozhilov, Karoliine Holter, Sarah Tilscher + 2 more
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage · Martin Jonás, Jan Strejcek, Marek Trtík, Lukás Urban
HaliVer: Deductive Verification and Scheduling Languages Join Forces · Lars B. van den Haak, Anton Wijs, Marieke Huisman, Mark van den Brand
Happy Ending: An Empty Hexagon in Every Set of 30 Points · Marijn J. H. Heule, Manfred Scheucher
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking · Muhammad Osama, Anton Wijs
IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL · Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli + 2 more
JPF: From 2003 to 2023 · Cyrille Artho, Pavel Parízek, Daohan Qu, Varadraj Galgali, Pu (Luke) Yi
Knor: reactive synthesis using Oink · Tom van Dijk, Feije van Abbema, Naum Tomov
Learning Explainable and Better Performing Representations of POMDP Strategies · Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretínský, Stefanie Mohr
Mata: A Fast and Simple Finite Automata Library · David Chocholatý, Tomás Fiedor, Vojtech Havlena, Lukás Holík, Martin Hruska, Ondrej Lengál + 1 more
Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution) · Raphaël Monat, Marco Milanese, Francesco Parolini, Jérôme Boillot, Abdelraouf Ouadjaout, Antoine Miné
Most General Winning Secure Equilibria Synthesis in Graph Games · Satya Prakash Nayak, Anne-Kathrin Schmuck
NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis · Matthias Cosler, Christopher Hahn, Ayham Omar, Frederik Schmitt
On Dependent Variables in Reactive Synthesis · S. Akshay, Eliyahu Basa, Supratik Chakraborty, Dror Fried
On-The-Fly Algorithm for Reachability in Parametric Timed Games · Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci, Jaco van de Pol
OxiDD - A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust · Nils Husung, Clemens Dubslaff, Holger Hermanns, Maximilian A. Köhl
PROTON: PRObes for Termination Or Not (Competition Contribution) · Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, R. Venkatesh, Supratik Chakraborty
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs · Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, Sebastian Junges
Provable Preimage Under-Approximation for Neural Networks · Xiyue Zhang, Benjie Wang, Marta Kwiatkowska
Rabin Games and Colourful Universal Trees · Rupak Majumdar, Irmak Saglam, K. S. Thejaswini
SWAT: Modular Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution) · Nils Loose, Felix Mächtle, Florian Sieck, Thomas Eisenbarth
Scalable Tree-based Register Automata Learning · Simon Dierl, Paul Fiterau-Brostean, Falk Howar, Bengt Jonsson, Konstantinos Sagonas, Fredrik Tåquist
Small Test Suites for Active Automata Learning · Loes Kruger, Sebastian Junges, Jurriaan Rot
SootUp: A Redesign of the Soot Static Analysis Framework · Kadiray Karakaya, Stefan Schott, Jonas Klauke, Eric Bodden, Markus Schmidt, Linghui Luo + 1 more
Speculative SAT Modulo SAT · Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
State of the Art in Software Verification and Witness Validation: SV-COMP 2024 · Dirk Beyer
Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution - (Competition Contribution) · Martin Jonás, Kristián Kumor, Jakub Novák, Jindrich Sedlácek, Marek Trtík, Lukás Zaoral + 2 more
TaSSAT: Transfer and Share SAT · Md. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule
Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution) · Levente Bajczi, Csanád Telbisz, Márk Somorjai, Zsófia Ádám, Mihály Dobos-Kovács, Dániel Szekeres + 2 more
Towards Safe Autonomous Driving: Model Checking a Behavior Planner during Development · Lukas König, Christian Heinzemann, Alberto Griggio, Michaela Klauck, Alessandro Cimatti, Franziska Henze + 4 more
Training for Verification: Increasing Neuron Stability to Scale DNN Verification · Dong Xu, Nusrat Jahan Mozumder, Hai Duong, Matthew B. Dwyer
Ultimate Automizer and the Abstraction of Bitwise Operations - (Competition Contribution) · Frank Schüssele, Manuel Bentele, Daniel Dietsch, Matthias Heizmann, Xinyu Jiang, Dominik Klumpp + 1 more
VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification · Mertcan Temel
Verification under TSO with an infinite Data Domain · Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Shashwat Garg
Weakest Precondition Inference for Non-Deterministic Linear Array Programs · Sumanth Prabhu, Deepak D'Souza, Supratik Chakraborty, R. Venkatesh, Grigory Fedyukovich
Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 - (Competition Contribution) · Paulína Ayaziová, Jan Strejcek
Z3-Noodler: An Automata-based String Solver · Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc