Abstract is missing.
- Combining Forces: How to Formally Verify Informally Defined Embedded SystemsPaula Herber, Timm Liebrenz, Julius Adelt. 3-22 [doi]
- Model Checking for Verification of Quantum CircuitsMingsheng Ying. 23-39 [doi]
- Verifying Secure Speculation in Isabelle/HOLMatt Griffin, Brijesh Dongol. 43-60 [doi]
- Two Mechanisations of WebAssembly 1.0Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner. 61-79 [doi]
- Probabilistic Verification of Neural Networks Against Group FairnessBing Sun, Jun Sun 0001, Ting Dai, Lijun Zhang. 83-102 [doi]
- BanditFuzz: Fuzzing SMT Solvers with Multi-agent Reinforcement LearningJoseph Scott, Trishal Sudula, Hammad Rehman, Federico Mora, Vijay Ganesh. 103-121 [doi]
- Formally Verified Safety Net for Waypoint Navigation Neural Network ControllersAlexei Kopylov, Stefan Mitsch, Aleksey Nogin, Michael Warren. 122-141 [doi]
- Model-Free Reinforcement Learning for Lexicographic Omega-Regular ObjectivesErnst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi 0001, Dominik Wojtczak. 142-159 [doi]
- Efficient Algorithms for Omega-Regular Energy GamesGal Amram, Shahar Maoz, Or Pistiner, Jan Oliver Ringert. 163-181 [doi]
- Generalizing Non-punctuality for Timed Temporal Logic with Freeze QuantifiersShankara Narayanan Krishna, Khushraj Madnani, Manuel Mazo, Paritosh K. Pandya. 182-199 [doi]
- Verified Quadratic Virtual Substitution for Real ArithmeticMatias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer. 200-217 [doi]
- Business Processes Meet Spatial Concerns: The sBPMN Verification FrameworkRim Saddem-yagoubi, Pascal Poizat, Sara Houhou. 218-234 [doi]
- Owicki-Gries Reasoning for C11 Programs with Relaxed DependenciesDaniel Wright, Mark Batty, Brijesh Dongol. 237-254 [doi]
- Integrating ADTs in KeY and Their Application to History-Based ReasoningJinting Bian, Hans-Dieter A. Hiep, Frank S. de Boer, Stijn de Gouw. 255-272 [doi]
- Identifying Overly Restrictive Matching Patterns in SMT-Based Program VerifiersAlexandra Bugariu, Arshavir Ter-Gabrielyan, Peter Müller 0001. 273-291 [doi]
- Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory ModelsNicholas Coughlin, Kirsten Winter, Graeme Smith. 292-310 [doi]
- Hybrid System Falsification for Multiple-Constraint Parameter Synthesis: A Gas Turbine Case StudySota Sato 0001, Atsuyoshi Saimen, Masaki Waga, Kenji Takao, Ichiro Hasuo. 313-329 [doi]
- Gaussian Process-Based Confidence Estimation for Hybrid System FalsificationZhenya Zhang, Paolo Arcaini. 330-348 [doi]
- Formal Verification of Intelligent Hybrid Systems that are Modeled with Simulink and the Reinforcement Learning ToolboxJulius Adelt, Timm Liebrenz, Paula Herber. 349-366 [doi]
- Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster ProofsSimon Foster 0001, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth. 367-386 [doi]
- Z3str4: A Multi-armed String SolverFederico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, Vijay Ganesh. 389-406 [doi]
- Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDAFelix A. Wolf, Malte Schwerhoff, Peter Müller 0001. 407-426 [doi]
- Formal Verification of a JavaCard Virtual Machine with Frama-CAdel Djoudi, Martin Hána, Nikolai Kosmatov. 427-444 [doi]
- Verification of the Incremental Merkle Tree Algorithm with DafnyFranck Cassez. 445-462 [doi]
- Congruence Relations for Büchi AutomataYong Li 0031, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang 0001. 465-482 [doi]
- Featured Team AutomataMaurice H. ter Beek, Guillermina Cledou, Rolf Hennicker, José Proença. 483-502 [doi]
- From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRETAnastasia Mavridou, Andreas Katis, Dimitra Giannakopoulou, David Kooi, Thomas Pressburger, Michael W. Whalen. 503-523 [doi]
- Fingerprinting Bluetooth Low Energy Devices via Active Automata LearningAndrea Pferscher, Bernhard K. Aichernig. 524-542 [doi]
- Trace Abstraction-Based Verification for Uninterpreted ProgramsWeijiang Hong, Zhenbang Chen, Yide Du, Ji Wang. 545-562 [doi]
- HStriver: A Very Functional Extensible Tool for the Runtime Verification of Real-Time Event StreamsFelipe Gorostiaga, César Sánchez. 563-580 [doi]
- Cabean 2.0: Efficient and Efficacious Control of Asynchronous Boolean NetworksCui Su, Jun Pang 0001. 581-598 [doi]
- Dynamic Reconfiguration via Typed ModalitiesIonut Tutu, Claudia Elena Chirita, José Luiz Fiadeiro. 599-615 [doi]
- On Lexicographic Proof Rules for Probabilistic TerminationKrishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný 0001, Jiri Zárevúcky, Dorde Zikelic. 619-639 [doi]
- Fuel in Markov Decision Processes (FiMDP): A Practical Approach to ConsumptionFrantisek Blahoudek, Murat Cubuktepe, Petr Novotný 0001, Melkior Ornik, Pranay Thangeda, Ufuk Topcu. 640-656 [doi]
- HyperProb: A Model Checker for Probabilistic HyperpropertiesOyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour. 657-666 [doi]
- The Probabilistic Termination Tool AmberMarcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács. 667-675 [doi]
- Model Checking Collision Avoidance of Nonlinear Autonomous VehiclesRong Gu, Cristina Seceleanu, Eduard Enoiu, Kristina Lundqvist. 676-694 [doi]
- Formal Verification of Complex Data Paths: An Industrial ExperienceCarl-Johan H. Seger. 697-716 [doi]
- Some Lessons Learned in the Industrialization of Formal Methods for Financial AlgorithmsGrant Olney Passmore. 717-721 [doi]
- Two Decades of Formal Methods in Industrial Products at BTC Embedded SystemsTino Teige, Andreas Eggers, Karsten Scheibler, Matthias Stasch, Udo Brockmeyer, Hans Jürgen Holberg, Tom Bienmüller. 725-729 [doi]
- Formal Analysis of Neural Network-Based Systems in the Aircraft DomainPanagiotis Kouvaros, Trent Kyono, Francesco Leofante, Alessio Lomuscio, Dragos D. Margineantu, Denis Osipychev, Yang Zheng 0001. 730-740 [doi]
- Formal Verification of Consensus in the Taurus Distributed DatabaseSong Gao, Bohua Zhan, Depeng Liu, Xuechao Sun, Yanan Zhi, David N. Jansen, Lijun Zhang 0001. 741-751 [doi]
- Combined Online Checking and Control Synthesis: A Study on a Vehicle Platoon TestbedJiawan Wang, Lei Bu, Shaopeng Xing, Yuming Wu, Xuandong Li. 752-762 [doi]
- Formally Guaranteed Tight Dynamic Future Occupancy of Autonomous VehiclesYousaf Rahman, Md Tawhid Bin Waez, Yuming Niu. 763-775 [doi]
- Divide et Impera: Efficient Synthesis of Cyber-Physical System Architectures from Formal ContractsCésar Augusto Ribeiro dos Santos, Tom Schrijvers, Amr Hany Saleh, Mike Nicolai. 776-787 [doi]
- Apply Formal Methods in Certifying the SyberX High-Assurance KernelWenjing Xu, Yongwang Zhao, Chengtao Cao, Jean Raphael Ngnie Sighom, Lei Wang, Zhe Jiang, Shihong Zou. 788-798 [doi]