default search action
29th TACAS@ETAPS 2023: Paris, France - Part II
- Sriram Sankaranarayanan
, Natasha Sharygina
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II. Lecture Notes in Computer Science 13994, Springer 2023, ISBN 978-3-031-30819-2
Tool Demos
- Alessandro Cimatti
EVA: a Tool for the Compositional Verification of AUTOSAR Models. 3-10 - Wenji Fang
WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification. 11-18 - Jelle Bouma
Multiparty Session Typing in Java, Deductively. 19-27 - Bastien Thomas, Ocan Sankur:
PyLTA: A Verification Tool for Parameterized Distributed Algorithms. 28-35 - Shengping Xiao, Chengyu Zhang
FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 Format. 36-43 - Wan J. Fokkink
Eclipse ESCET™: The Eclipse Supervisory Control Engineering Toolkit. 44-52
Combinatorial Optimization/Theorem Proving
- João Cortes
New Core-Guided and Hitting Set Algorithms for Multi-Objective Combinatorial Optimization. 55-73 - Alexander Bentkamp
Verified reductions for optimization. 74-92 - Xavier Denis
Specifying and Verifying Higher-order Rust Iterators. 93-110 - Petar Vukmirovic
Extending a High-Performance Prover to Higher-Order Logic. 111-129
Tools (Regular Papers)
- Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
The WhyRel Prototype for Modular Relational Verification of Pointer Programs. 133-151 - Dirk Beyer
Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. 152-172 - Martin Mariusz Lester
CoPTIC: Constraint Programming Translated Into C. 173-191 - Michaël Cadilhac
Acacia-Bonsai: A Modern Implementation of Downset-Based LTL Realizability. 192-207
Synthesis
- Ashwani Anand, Kaushik Mallik, Satya Prakash Nayak, Anne-Kathrin Schmuck:
Computing Adequately Permissive Assumptions for Synthesis. 211-228 - Yuning Wang, He Zhu
Verification-guided Programmatic Controller Synthesis. 229-250 - Philippe Heim
Taming Large Bounds in Synthesis from Bounded-Liveness Specifications. 251-269 - Ameer Hamza
Lockstep Composition for Unbalanced Loops. 270-288 - Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, Roopsha Samanta:
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification. 289-308 - Mrudula Balachander, Emmanuel Filiot, Jean-François Raskin:
LTL Reactive Synthesis with a Few Hints. 309-328 - Ocan Sankur:
Timed Automata Verification and Synthesis via Finite Automata Learning. 329-349
Graphs/Probabilistic Systems
- Casper Abild Larsen, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume Jakobsen, Jaco van de Pol
A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. 353-371 - Oliver Kullmann, Ankit Shukla:
Transforming Quantified Boolean Formulas Using Biclique Covers. 372-390 - Tobias Winkler
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration. 391-409 - Kevin Batz
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. 410-429
Runtime Monitoring/Program Analysis
- Pantazis Deligiannis
Industrial-Strength Controlled Concurrency Testing for sc C tt # Programs with sc Coyote. 433-452 - Kalmer Apinis, Vesal Vojdani:
Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis. 453-472 - Leonardo Lima
Explainable Online Monitoring of Metric Temporal Logic. 473-491
12th Competition on Software Verification - SV-COMP 2023
- Dirk Beyer
Competition on Software Verification and Witness Validation: SV-COMP 2023. 495-522 - Paulína Ayaziová
Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation - (Competition Contribution). 523-528 - Viktor Malík
2LS: Arrays and Loop Unwinding - (Competition Contribution). 529-534 - Marek Chalupa
Bubaak: Runtime Monitoring of Program Verifiers - (Competition Contribution). 535-540 - Fatimah Aljaafari
EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs - (Competition Contribution). 541-546 - Simmo Saan
Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution). 547-552 - Soha Hussein
Java Ranger: Supporting String and Array Operations in Java Ranger (Competition Contribution). 553-558 - Gidon Ernst
Korn - Software Verification with Horn Clauses (Competition Contribution). 559-564 - Raphaël Monat
Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution). 565-570 - Jie Su
PIChecker: A POR and Interpolation based Verifier for Concurrent Programs (Competition Contribution). 571-576 - Matthias Heizmann
Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution). 577-581 - Daniel Dietsch
Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution). 582-587 - Priyanka Darke
VeriAbsL: Scalable Verification by Abstraction and Strategy Prediction (Competition Contribution). 588-593 - Ravindra Metta
VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution). 594-599
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-26 00:34 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: