Abstract is missing.
- A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic UncertaintiesRupak Majumdar, Kaushik Mallik, Mateusz Rychlicki, Anne-Kathrin Schmuck, Sadegh Soudjani. 3-15 [doi]
- Automated Tail Bound Analysis for Probabilistic Recurrence RelationsYican Sun, Hongfei Fu 0001, Krishnendu Chatterjee, Amir Kafshdar Goharshady. 16-39 [doi]
- Compositional Probabilistic Model Checking with String Diagrams of MDPsKazuki Watanabe 0003, Clovis Eberhart, Kazuyuki Asada, Ichiro Hasuo. 40-61 [doi]
- Efficient Sensitivity Analysis for Parametric Robust Markov ChainsThom S. Badings, Sebastian Junges, Ahmadreza Marandi, Ufuk Topcu, Nils Jansen 0001. 62-85 [doi]
- MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety ObjectivesS. Akshay 0001, Krishnendu Chatterjee, Tobias Meggendorfer, Dorde Zikelic. 86-112 [doi]
- Search and Explore: Symbiotic Policy Synthesis in POMDPsRoman Andriushchenko, Alexander Bork, Milan Ceska 0002, Sebastian Junges, Joost-Pieter Katoen, Filip Macák. 113-135 [doi]
- AutoQ: An Automata-Based Quantum Circuit VerifierYu-Fang Chen 0001, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai. 139-153 [doi]
- Bounded Verification for Finite-Field-Blasting - In a Compiler for Zero Knowledge ProofsAlex Ozdemir, Riad S. Wahby, Fraser Brown, Clark W. Barrett. 154-175 [doi]
- Formally Verified EVM Block-OptimizationsElvira Albert, Samir Genaim, Daniel Kirchner, Enrique Martin-Martin. 176-189 [doi]
- SR-SFLL: Structurally Robust Stripped Functionality Logic LockingGourav Takhar, Subhajit Roy 0001. 190-212 [doi]
- Symbolic Quantum Simulation with QuasimodoMeghana Sistla, Swarat Chaudhuri, Thomas W. Reps. 213-225 [doi]
- Verifying the Verifier: eBPF Range Analysis VerificationHarishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, Santosh Nagarakatte. 226-251 [doi]
- Automated Verification of Correctness for Masked Arithmetic ProgramsMingyang Liu, Fu Song, Taolue Chen. 255-280 [doi]
- Automatic Program Instrumentation for Automatic VerificationJesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Philipp Rümmer. 281-304 [doi]
- Boolean Abstractions for Realizability Modulo TheoriesAndoni Rodríguez, César Sánchez 0001. 305-328 [doi]
- Certified Verification for Algebraic AbstractionMing-Hsien Tsai 0001, Yu-Fu Fu, Jiaxiang Liu 0001, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang. 329-349 [doi]
- Complete Multiparty Session Type Projection with AutomataElaine Li, Felix Stutz, Thomas Wies, Damien Zufferey. 350-373 [doi]
- Early Verification of Legal Compliance via Bounded Satisfiability CheckingNick Feng, Lina Marsso, Mehrdad Sabetzadeh, Marsha Chechik. 374-396 [doi]
- Formula Normalizations in VerificationSimon Guilloud, Mario Bucev, Dragana Milovancevic, Viktor Kuncak. 398-422 [doi]
- Kratos2: An SMT-Based Model Checker for Imperative ProgramsAlberto Griggio, Martin Jonás. 423-436 [doi]
- Making sf IP=sf PSPACE Practical: Efficient Interactive Protocols for BDD AlgorithmsEszter Couillard, Philipp Czerner, Javier Esparza, Rupak Majumdar. 437-458 [doi]
- Ownership Guided C to Rust TranslationHanliang Zhang, Cristina David, Yijun Yu, Meng Wang. 459-482 [doi]
- R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and SoftwareChris Johannsen, Phillip H. Jones, Brian Kempa, Kristin Yvonne Rozier, Pei Zhang 0009. 483-497 [doi]