Abstract is missing.
- DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural NetworksDivya Gopinath, Guy Katz, Corina S. Pasareanu, Clark Barrett. 3-19 [doi]
- Formal Specification for Deep Neural NetworksSanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, Xiangyu Yue. 20-34 [doi]
- Optimal Proofs for Linear Temporal Logic on Lasso WordsDavid A. Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel. 37-55 [doi]
- What's to Come is Still Unsure - Synthesizing Controllers Resilient to Delayed InteractionMingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan. 56-74 [doi]
- A Formally Verified Motion Planner for Autonomous VehiclesAlbert Rizaldi, Fabian Immler, Bastian Schürmann, Matthias Althoff. 75-90 [doi]
- Robustness Testing of Intermediate VerifiersYuting Chen, Carlo A. Furia. 91-108 [doi]
- Simulation Algorithms for Symbolic AutomataLukás Holík, Ondrej Lengál, Juraj Síc, Margus Veanes, Tomás Vojnar. 109-125 [doi]
- Quantitative Projection Coverage for Testing ML-enabled Autonomous SystemsChih-Hong Cheng, Chung-Hao Huang, Hirotoshi Yasuoka. 126-142 [doi]
- Recursive Online Enumeration of All Minimal Unsatisfiable SubsetsJaroslav Bendík, Ivana Cerná, Nikola Benes. 143-159 [doi]
- Synthesis in pMDPs: A Tale of 1001 ParametersMurat Cubuktepe, Nils Jansen 0001, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. 160-176 [doi]
- Temporal Logic Verification of Stochastic Systems Using Barrier CertificatesPushpak Jagtap, Sadegh Soudjani, Majid Zamani. 177-193 [doi]
- Bisimilarity Distances for Approximate Differential PrivacyDmitry Chistikov, Andrzej S. Murawski, David Purser. 194-210 [doi]
- A Symbolic Algorithm for Lazy Synthesis of Eager StrategiesSwen Jacobs, Mouhammad Sakr. 211-227 [doi]
- Modular Verification of Concurrent Programs via Sequential Model CheckingDan Rasin, Orna Grumberg, Sharon Shoham. 228-247 [doi]
- Quantifiers on DemandArie Gurfinkel, Sharon Shoham, Yakir Vizel. 248-266 [doi]
- Signal Convolution LogicSimone Silvetti, Laura Nenzi, Ezio Bartocci, Luca Bortolussi. 267-283 [doi]
- Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional SpacesBernard Boigelot, Isabelle Mainz. 284-299 [doi]
- Accelerated Model Checking of Parametric Markov ChainsPaul Gainer, Ernst Moritz Hahn, Sven Schewe. 300-316 [doi]
- Continuous-Time Markov Decisions Based on Partial ExplorationPranav Ashok, Yuliya Butkova, Holger Hermanns, Jan Kretínský. 317-334 [doi]
- A Fragment of Linear Temporal Logic for Universal Very Weak AutomataKeerthi Adabala, Rüdiger Ehlers. 335-351 [doi]
- Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with DivisibilityAnthony W. Lin, Rupak Majumdar. 352-369 [doi]
- Round-Bounded Control of Parameterized SystemsBenedikt Bollig, Mathieu Lehaut, Nathalie Sznajder. 370-386 [doi]
- PSense: Automatic Sensitivity Analysis for Probabilistic ProgramsZixin Huang, Zhenbang Wang, Sasa Misailovic. 387-403 [doi]
- Information Leakage in Arbiter ProtocolsNestan Tsiskaridze, Lucas Bang, Joseph McMahan, Tevfik Bultan, Timothy Sherwood. 404-421 [doi]
- Neural State Classification for Hybrid SystemsDung Phan, Nicola Paoletti, Timothy Zhang, Radu Grosu, Scott A. Smolka, Scott D. Stoller. 422-440 [doi]
- Bounded Synthesis of Reactive ProgramsCarsten Gerstacker, Felix Klein 0001, Bernd Finkbeiner. 441-457 [doi]
- Maximum Realizability for Linear Temporal Logic SpecificationsRayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu. 458-475 [doi]
- Ranking and Repulsing Supermartingales for Reachability in Probabilistic ProgramsToru Takisaka, Yuichiro Oyabu, Natsuki Urabe, Ichiro Hasuo. 476-493 [doi]
- Bounded Synthesis of Register TransducersAyrat Khalimov, Benedikt Maderbacher, Roderick Bloem. 494-510 [doi]
- EthIR: A Framework for High-Level Analysis of Ethereum BytecodeElvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey. 513-520 [doi]
- MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \exists ^*\forall ^* ∃ ∗ ∀ ∗ FragmentBernd Finkbeiner, Christopher Hahn, Tobias Hans. 521-527 [doi]
- Verifying Rust Programs with SMACKMarek S. Baranowski, Shaobo He, Zvonimir Rakamaric. 528-535 [doi]
- S BIP 2.0: Statistical Model Checking Stochastic Real-Time SystemsBraham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Axel Legay, Saddek Bensalem. 536-542 [doi]
- Owl: A Library for \omega -Words, Automata, and LTLJan Kretínský, Tobias Meggendorfer, Salomon Sickert. 543-550 [doi]
- EVE: A Tool for Temporal Equilibrium AnalysisJulian Gutierrez 0001, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge. 551-557 [doi]