Abstract is missing.
- Resource Analysis: From Sequential to Concurrent and Distributed ProgramsElvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, Guillermo Román-Díez. 3-17 [doi]
- AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons LearnedWerner Damm. 18-19 [doi]
- Automated Circular Assume-Guarantee ReasoningKaram Abd Elkader, Orna Grumberg, Corina S. Pasareanu, Sharon Shoham. 23-39 [doi]
- Towards Formal Verification of Orchestration Computations Using the K FrameworkMusab A. AlTurki, Omar Alzuhaibi. 40-56 [doi]
- Narrowing Operators on Template Abstract DomainsGianluca Amato, Simone Di Nardo Di Maio, Maria Chiara Meo, Francesca Scozzari. 57-72 [doi]
- Detection of Design Flaws in the Android Permission Protocol Through Bounded VerificationHamid Bagheri, Eunsuk Kang, Sam Malek, Daniel Jackson. 73-89 [doi]
- Privacy by Design in Practice: Reasoning about Privacy Properties of Biometric System ArchitecturesJulien Bringer, Hervé Chabanne, Daniel Le Métayer, Roch Lescuyer. 90-107 [doi]
- A Specification Language for Static and Runtime Verification of Data and Control PropertiesWolfgang Ahrendt, Jesús Mauricio Chimento, Gordon J. Pace, Gerardo Schneider. 108-125 [doi]
- Certificates for Parameterized Model CheckingSylvain Conchon, Alain Mebsout, Fatiha Zaïdi. 126-142 [doi]
- Safety, Liveness and Run-Time Refinement for Modular Process-Aware Information Systems with Dynamic Sub ProcessesSøren Debois, Thomas T. Hildebrandt, Tijs Slaats. 143-160 [doi]
- Verifying Opacity of a Transactional Mutex LockJohn Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim. 161-177 [doi]
- A Framework for Correctness Criteria on Weak Memory ModelsJohn Derrick, Graeme Smith. 178-194 [doi]
- Semantics-Preserving Simplification of Real-World Firewall Rule SetsCornelius Diekmann, Lars Hupel, Georg Carle. 195-212 [doi]
- Parameter Synthesis Through Temporal Logic SpecificationsThao Dang, Tommaso Dreossi, Carla Piazza. 213-230 [doi]
- Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTLXiaoning Du, Yang Liu, Alwen Tiu. 231-247 [doi]
- Probabilistic Bisimulation for Realistic SchedulersChristian Eisentraut, Jens Chr. Godskesen, Holger Hermanns, Lei Song, Lijun Zhang 0001. 248-264 [doi]
- QPMC: A Model Checker for Quantum Programs and ProtocolsYuan Feng, Ernst Moritz Hahn, Andrea Turrini, Lijun Zhang. 265-272 [doi]
- Automated Verification of RPC Stub CodeMatthew Fernandez, June Andronick, Gerwin Klein, Ihor Kuz. 273-290 [doi]
- Property-Driven Fence Insertion Using Reorder Bounded Model CheckingSaurabh Joshi 0001, Daniel Kroening. 291-307 [doi]
- Verifying the Safety of a Flight-Critical SystemGuillaume Brat, David H. Bushnell, Misty Davies, Dimitra Giannakopoulou, Falk Howar, Temesghen Kahsai. 308-324 [doi]
- Proving Safety with Trace Automata and Bounded Model CheckingDaniel Kroening, Matt Lewis, Georg Weissenbacher. 325-341 [doi]
- Verifying Parameterized Timed Security ProtocolsLi Li, Jun Sun, Yang Liu, Jin Song Dong. 342-359 [doi]
- Abstraction of Elementary Hybrid Systems by Variable TransformationJiang Liu 0009, Naijun Zhan, Hengjun Zhao, Liang Zou. 360-377 [doi]
- Using Real-Time Maude to Model Check Energy Consumption BehaviorShin Nakajima. 378-394 [doi]
- Static Differential Program Analysis for Software-Defined NetworksTim Nelson, Andrew D. Ferguson, Shriram Krishnamurthi. 395-413 [doi]
- A Fully Verified Container LibraryNadia Polikarpova, Julian Tschannen, Carlo A. Furia. 414-434 [doi]
- Counterexamples for Expected RewardsTim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. 435-452 [doi]
- The Semantics of Cardinality-Based Feature Models via Formal LanguagesAliakbar Safilian, Tom Maibaum, Zinovy Diskin. 453-469 [doi]
- Axiomatization of Typed First-Order LogicPeter H. Schmitt, Mattias Ulbrich. 470-486 [doi]
- Model-Based Problem Solving for University Timetable Validation and ImprovementDavid Schneider, Michael Leuschel, Tobias Witt. 487-495 [doi]
- Certified Reasoning with InfinityAsankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin. 496-513 [doi]
- Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical SystemsAndrew Sogokon, Paul B. Jackson. 514-531 [doi]
- Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor ExpansionsAlexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan. 532-550 [doi]
- Static Optimal Scheduling for Synchronous Data Flow Graphs with Model CheckingXueyang Zhu, Rongjie Yan, Yu-Lei Gu, Jian Zhang, Wenhui Zhang, Guangquan Zhang. 551-569 [doi]
- Eliminating Static Analysis False Positives Using Loop Abstraction and Bounded Model CheckingBharti Chimdyalwar, Priyanka Darke, Anooj Chavda, Sagar Vaghani, Avriti Chauhan. 573-576 [doi]
- Autofunk: An Inference-Based Formal Model Generation Framework for Production SystemsWilliam Durand, Sébastien Salva. 577-580 [doi]
- Software Development and Authentication for Arms Control Information BarriersNeil Evans. 581-584 [doi]
- Analyzing the Restart Behavior of Industrial Control ApplicationsStefan Hauck-Stattelmann, Sebastian Biallas, Bastian Schlich, Stefan Kowalewski, Raoul Jetley. 585-588 [doi]
- Case Study: Static Security Analysis of the Android Goldfish KernelTao Liu, Ralf Huuck. 589-592 [doi]
- Practices for Formal Models as Documents: Evolution of VDM Application to "Mobile FeliCa" IC Chip FirmwareTaro Kurita, Fuyuki Ishikawa, Keijiro Araki. 593-596 [doi]
- Formal Virtual Modelling and Data Verification for Supervision SystemsThierry Lecomte. 597-600 [doi]
- Using Simulink Design Verifier for Automatic Generation of Requirements-Based TestsBruno Miranda, Henrique Masini, Rodrigo Reis. 601-604 [doi]
- Formalizing the Concept Phase of Product DevelopmentMathijs Schuts, Jozef Hooman. 605-608 [doi]