Abstract is missing.
- Verification of LSTM Neural Networks with Non-linear Activation FunctionsFarzaneh Moradkhani, Connor Fibich, Martin Fränzle. 1-15 [doi]
- Open- and Closed-Loop Neural Network Verification Using Polynomial ZonotopesNiklas Kochdumper, Christian Schilling 0001, Matthias Althoff, Stanley Bak. 16-36 [doi]
- Verifying Attention Robustness of Deep Neural Networks Against Semantic PerturbationsSatoshi Munakata, Caterina Urban, Haruki Yokoyama, Koji Yamamoto, Kazuki Munakata. 37-61 [doi]
- Formalizing Piecewise Affine Activation Functions of Neural Networks in CoqAndrei Aleksandrov, Kim Völlinger. 62-78 [doi]
- Verifying an Aircraft Collision Avoidance Neural Network with MarabouCong Liu, Darren D. Cofer, Denis Osipychev. 79-85 [doi]
- Strategy Synthesis in Markov Decision Processes Under Limited Sampling AccessChristel Baier, Clemens Dubslaff, Patrick Wienhöft, Stefan J. Kiebel. 86-103 [doi]
- Learning Symbolic Timed Models from Concrete Timed DataSimon Dierl, Falk Maria Howar, Sean Kauffman, Martin Kristjansen, Kim Guldstrand Larsen, Florian Lorber, Malte Mauritz. 104-121 [doi]
- Reward Shaping from Hybrid Systems Models in Reinforcement LearningMarian Qian, Stefan Mitsch. 122-139 [doi]
- Conservative Safety Monitors of Stochastic Dynamical SystemsMatthew Cleaveland, Oleg Sokolsky, Insup Lee 0001, Ivan Ruchkin. 140-156 [doi]
- Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying SystemsElias Khalife, Pierre-Loïc Garoche, Mazen Farhood. 157-173 [doi]
- Reasoning with Metric Temporal Logic and Resettable Skewed ClocksAlberto Bombardelli, Stefano Tonetta. 174-190 [doi]
- Centralized Multi-agent Synthesis with Spatial Constraints via Mixed-Integer Quadratic ProgrammingAlexandra Forsey-Smerek, Ho Chit Siu, Kevin Leahy 0001. 191-206 [doi]
- A Framework for Policy Based NegotiationAnna Fritz, Perry Alexander. 207-223 [doi]
- Rewrite-Based Decomposition of Signal Temporal Logic SpecificationsKevin Leahy 0001, Makai Mann, Cristian Ioan Vasile. 224-240 [doi]
- Quantitative Verification and Strategy Synthesis for BDI AgentsBlair Archibald, Muffy Calder, Michele Sevegnani, Mengwei Xu. 241-259 [doi]
- Multi-objective Task Assignment and Multiagent Planning with Hybrid GPU-CPU AccelerationThomas Robinson, Guoxin Su. 260-277 [doi]
- Reasoning over Test Specifications Using Assume-Guarantee ContractsApurva Badithela, Josefine B. Graebener, Inigo Incer, Richard M. Murray. 278-294 [doi]
- From the Standards to Silicon: Formally Proved Memory ControllersFelipe Lisboa Malaquias, Mihail Asavoae, Florian Brandner. 295-311 [doi]
- Formalising Liveness Properties in Event-B with the Reflexive EB4EB FrameworkPeter Riviere, N. K. Singh, Yamine Aït Ameur, Guillaume Dupont. 312-331 [doi]
- Formalized High Level Synthesis with Applications to Cryptographic HardwareWilliam L. Harrison, Ian Blumenfeld, Eric Bond, Chris Hathhorn, Paul Li, May Torrence, Jared Ziegler. 332-352 [doi]
- From Natural Language Requirements to the Verification of Programmable Logic Controllers: Integrating FRET into PLCverifZsófia Ádám, Ignacio D. Lopez-Miguel, Anastasia Mavridou, Thomas Pressburger, Marcin Bes, Enrique Blanco Viñuela, Andreas Katis, Jean-Charles Tournier, Khanh V. Trinh, Borja Fernández Adiego. 353-360 [doi]
- Automata-Based Software Model Checking of HyperpropertiesBernd Finkbeiner, Hadar Frenkel, Jana Hofmann, Janine Lohse. 361-379 [doi]
- Condition Synthesis Realizability via Constrained Horn ClausesBat-Chen Rothenberg, Orna Grumberg, Yakir Vizel, Eytan Singher. 380-396 [doi]
- A Toolkit for Automated Testing of DafnyAleksandr Fedchin, Tyler Dean, Jeffrey S. Foster, Eric Mercer, Zvonimir Rakamaric, Giles Reger, Neha Rungta, Robin Salkeld, Lucas Wagner, Cassidy Waldrip. 397-413 [doi]
- Verified ALL(*) Parsing with Semantic Actions and Dynamic Input ValidationSam Lasser, Chris Casinghino, Derek Egolf, Kathleen Fisher, Cody Roux. 414-429 [doi]
- Subtropical Satisfiability for SMT SolvingJasper Nalbach, Erika Ábrahám. 430-446 [doi]
- A Linear Weight Transfer Rule for Local SearchMd. Solimul Chowdhury, Cayden R. Codel, Marijn J. H. Heule. 447-463 [doi]
- Adiar 1.1 - Zero-Suppressed Decision Diagrams in External MemorySteffan Christ Sølvsten, Jaco van de Pol. 464-471 [doi]
- Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search ProblemEnrico Lipparini, Stefan Ratschan. 472-488 [doi]