Abstract is missing.
- Symbolic Computation in Automated Program ReasoningLaura Kovács. 3-9 [doi]
- The Next Big Thing: From Embedded Systems to Embodied ActorsHarald Ruess. 10-25 [doi]
- Intelligent and Dependable Decision-Making Under UncertaintyNils Jansen 0001. 26-36 [doi]
- A Coq Formalization of Lebesgue Induction Principle and Tonelli's TheoremSylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine. 39-55 [doi]
- Railway Scheduling Using Boolean Satisfiability Modulo SimulationsTomás Kolárik, Stefan Ratschan. 56-73 [doi]
- SMT Sampling via Model-Guided ApproximationMatan Peled, Bat-Chen Rothenberg, Shachar Itzhaky. 74-91 [doi]
- Efficient SMT-Based Network Fault Tolerance VerificationYu Liu, Pavle Subotic, Emmanuel Letier, Sergey Mechtaev, Abhik Roychoudhury. 92-100 [doi]
- Formalising the Prevention of Microarchitectural Timing Channels by Operating SystemsRobert Sison, Scott Buckley, Toby Murray, Gerwin Klein, Gernot Heiser. 103-121 [doi]
- Can We Communicate? Using Dynamic Logic to Verify Team AutomataMaurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença. 122-141 [doi]
- The ScalaFix Equation SolverGianluca Amato, Francesca Scozzari. 142-159 [doi]
- HHLPy: Practical Verification of Hybrid Systems Using Hoare LogicHuanhuan Sheng, Alexander Bentkamp, Bohua Zhan. 160-178 [doi]
- symQV: Automated Symbolic Verification of Quantum ProgramsFabian Bauer-Marquart, Stefan Leue, Christian Schilling 0001. 181-198 [doi]
- sfPFL: A Probabilistic Logic for Fault TreesStefano M. Nicoletti, Milan Lopuhaä-Zwakenberg, Ernst Moritz Hahn, Mariëlle Stoelinga. 199-221 [doi]
- Energy Büchi ProblemsSven Dziadek, Uli Fahrenberg, Philipp Schlehuber-Caissier. 222-239 [doi]
- QMaude: Quantitative Specification and Verification in Rewriting LogicRubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto Verdejo. 240-259 [doi]
- Minimisation of Spatial Models Using Branching BisimilarityVincenzo Ciancia, Jan Friso Groote, Diego Latella, Mieke Massink, Erik P. de Vink. 263-281 [doi]
- Reasoning About Promises in Weak Memory Models with Event StructuresHeike Wehrheim, Lara Bargmann, Brijesh Dongol. 282-300 [doi]
- A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory ModelsRobert J. Colvin. 301-320 [doi]
- VeyMont: Parallelising Verified Programs Instead of Verifying Parallel ProgramsPetra van den Bos, Sung-Shik Jongmans. 321-339 [doi]
- Verifying Functional Correctness Properties at the Level of Java BytecodeMarco Paganoni, Carlo A. Furia. 343-363 [doi]
- Abstract Alloy InstancesJan Oliver Ringert, Allison Sullivan. 364-382 [doi]
- Monitoring the Internet ComputerDavid A. Basin, Daniel Stefan Dietiker, Srdan Krstic, Yvonne Anne Pignolet, Martin Raszyk, Joshua Schneider 0001, Arshavir Ter-Gabrielyan. 383-402 [doi]
- Word Equations in Synergy with Regular ConstraintsFrantisek Blahoudek, Yu-Fang Chen 0001, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc. 403-423 [doi]
- Verifying Feedforward Neural Networks for Classification in Isabelle/HOLAchim D. Brucker, Amy Stell. 427-444 [doi]
- SMPT: A Testbed for Reachability Methods in Generalized Petri NetsNicolas Amat, Silvano Dal-Zilio. 445-453 [doi]
- The Octatope Abstract Domain for Verification of Neural NetworksStanley Bak, Taylor Dohmen, K. Subramani, Ashutosh Trivedi 0001, Alvaro Velasquez, Piotr Wojciechowski 0002. 454-472 [doi]
- Program Semantics and Verification Technique for AI-Centred ProgramsSolofomampionona Fortunat Rajaona, Ioana Boureanu, Vadim Malvone, Francesco Belardinelli. 473-491 [doi]
- Tableaux for Realizability of Safety SpecificationsMontserrat Hermo, Paqui Lucio, César Sánchez 0001. 495-513 [doi]
- A Decision Diagram Operation for ReachabilitySebastiaan Brand, Thomas Bäck, Alfons Laarman. 514-532 [doi]
- Formal Modelling of Safety Architecture for Responsibility-Aware Autonomous Vehicle via Event-B RefinementTsutomu Kobayashi, Martin Bondu, Fuyuki Ishikawa. 533-549 [doi]
- A Runtime Environment for Contract AutomataDavide Basile 0001, Maurice H. ter Beek. 550-567 [doi]
- Formal and Executable Semantics of the Ethereum Virtual Machine in DafnyFranck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce 0001, Horacio Mijail Anton Quiles. 571-583 [doi]
- Shifting Left for Early Detection of Machine-Learning BugsBen Liblit, Linghui Luo, Alejandro Molina, Rajdeep Mukherjee, Zachary Patterson, Goran Piskachev, Martin Schäf, Omer Tripp, Willem Visser. 584-597 [doi]
- A Systematic Approach to Automotive SecurityMasoud Ebrahimi 0002, Stefan Marksteiner, Dejan Nickovic, Roderick Bloem, David Schögler, Philipp Eisner, Samuel Sprung, Thomas Schober, Sebastian Chlup, Christoph Schmittner, Sandra König. 598-609 [doi]
- Specification-Guided Critical Scenario Identification for Automated DrivingAdam Molin, Edgar A. Aguilar, Dejan Nickovic, Mengjia Zhu, Alberto Bemporad, Hasan Esen. 610-621 [doi]
- Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural NetworksVahid Hashemi, Jan Kretínský, Sabine Rieder, Jessica Schmidt. 622-634 [doi]
- Backdoor Mitigation in Deep Neural Networks via Strategic RetrainingAkshay Dhonthi, Ernst Moritz Hahn, Vahid Hashemi. 635-647 [doi]
- veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection SystemGuy Amir, Ziv Freund, Guy Katz, Elad Mandelbaum, Idan Refaeli. 648-656 [doi]