Abstract is missing.
- Adversarial Robustness Certification for Bayesian Neural NetworksMatthew Wicker, Andrea Patane, Luca Laurenti, Marta Kwiatkowska. 3-28 [doi]
- Getting Chip Card Payments RightDavid A. Basin, Xenia Hofmeier, Ralf Sasse, Jorge Toro-Pozo. 29-51 [doi]
- A Local Search Algorithm for MaxSMT(LIA)Xiang He, Bohan Li 0002, Mengyu Zhao, Shaowei Cai 0001. 55-72 [doi]
- Integrating Loop Acceleration Into Bounded Model CheckingFlorian Frohn, Jürgen Giesl. 73-91 [doi]
- Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic SetsHao Wu, Jie Wang 0037, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan. 92-110 [doi]
- Practical Approximate Quantifier Elimination for Non-linear Real ArithmeticS. Akshay 0001, Supratik Chakraborty, Amir Kafshdar Goharshady, R. Govind 0001, Harshit J. Motwani, Sai Teja Varanasi. 111-130 [doi]
- A Divide-and-Conquer Approach to Variable Elimination in Linear Real ArithmeticValentin Promies, Erika Ábrahám. 131-148 [doi]
- Free Facts: An Alternative to Inefficient Axioms in DafnyTabea Bordis, K. Rustan M. Leino. 151-169 [doi]
- Understanding Synthesized Reactive Systems Through InvariantsRüdiger Ehlers. 170-187 [doi]
- Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious AlgorithmsPengbo Yan, Toby Murray, Olga Ohrimenko, Van-Thuan Pham, Robert Sison. 188-205 [doi]
- Efficient Formally Verified Maximal End Component Decomposition for MDPsArnd Hartmanns, Bram Kohlen, Peter Lammich. 206-225 [doi]
- Introducing SWIRL: An Intermediate Representation Language for Scientific WorkflowsIacopo Colonnelli, Doriana Medic, Alberto Mulone, Viviana Bono, Luca Padovani, Marco Aldinucci. 226-244 [doi]
- Fast Attack Graph Defense Localization via BisimulationNimrod Busany, Rafi Shalom, Dan Klein, Shahar Maoz. 245-263 [doi]
- State Matching and Multiple References in Adaptive Active Automata LearningLoes Kruger, Sebastian Junges, Jurriaan Rot. 267-284 [doi]
- Automated Repair of Information Flow Security in Android Implicit Inter-App CommunicationAbhishek Tiwari 0001, Jyoti Prakash, Zhen Dong, Carlo A. Furia. 285-303 [doi]
- Learning Branching-Time Properties in CTL and ATL via Constraint SolvingBenjamin Bordais, Daniel Neider, Rajarshi Roy 0002. 304-323 [doi]
- A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural NetworksEric Goubault, Sylvie Putot. 324-342 [doi]
- Certified Quantization Strategy Synthesis for Neural NetworksYedi Zhang, Guangke Chen, Fu Song, Jun Sun 0001, Jin Song Dong. 343-362 [doi]
- Partially Observable Stochastic Games with Neural Perception MechanismsRui Yan 0002, Gabriel Santos, Gethin Norman, David Parker 0001, Marta Kwiatkowska. 363-380 [doi]
- Bridging Dimensions: Confident Reachability for High-Dimensional ControllersYuang Geng, Jake Brandon Baldauf, Souradeep Dutta, Chao Huang 0015, Ivan Ruchkin. 381-402 [doi]
- VeriQR: A Robustness Verification Tool for quantum Machine Learning ModelsYanling Lin, Ji Guan 0001, Wang Fang, Mingsheng Ying, Zhaofeng Su. 403-421 [doi]
- Formal Semantics and Analysis of Multitask PLC ST Programs with PreemptionJaeseo Lee, Kyungmin Bae. 425-442 [doi]
- Accurate Static Data Race Detection for CEmerson Sales, Omar Inverso, Emilio Tuosto. 443-462 [doi]
- cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test CasesPedro Orvalho, Mikolás Janota, Vasco M. Manquinho. 463-481 [doi]
- Detecting Speculative Execution Vulnerabilities on Weak Memory ModelsNicholas Coughlin, Kait Lam, Graeme Smith 0001, Kirsten Winter. 482-500 [doi]
- Staged Specification Logic for Verifying Higher-Order Imperative ProgramsDarius Foo, Yahui Song, Wei-Ngan Chin. 501-518 [doi]
- Unifying Weak Memory Verification Using PotentialsLara Bargmann, Brijesh Dongol, Heike Wehrheim. 519-537 [doi]
- Proving Functional Program Equivalence via Directed Lemma SynthesisYican Sun, Ruyi Ji, Jian Fang, Xuanlin Jiang, Mingshuai Chen, Yingfei Xiong 0001. 538-557 [doi]
- Reachability Analysis for Multiloop Programs Using Transition Power AbstractionKonstantin Britikov, Martin Blicha, Natasha Sharygina, Grigory Fedyukovich. 558-576 [doi]
- Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal LogicBen Greenman, Siddhartha Prasad, Antonio Di Stasio 0001, Shufang Zhu 0001, Giuseppe De Giacomo, Shriram Krishnamurthi, Marco Montali, Tim Nelson, Milda Zizyte. 579-599 [doi]
- Sound and Complete Witnesses for Template-Based Verification of LTL Properties on Polynomial ProgramsKrishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Dorde Zikelic. 600-619 [doi]
- The Opacity of Timed AutomataJie An 0001, Qiang Gao, Lingtai Wang, Naijun Zhan, Ichiro Hasuo. 620-637 [doi]
- Parameterized Verification of Round-Based Distributed Algorithms via Extended Threshold AutomataTom Baumeister, Paul Eichler, Swen Jacobs, Mouhammad Sakr, Marcus Völp. 638-657 [doi]
- The Nonexistence of Unicorns and Many-Sorted Löwenheim-Skolem TheoremsBenjamin Przybocki, Guilherme Vicentin de Toledo, Yoni Zohar, Clark W. Barrett. 658-675 [doi]