Abstract is missing.
- Improved State Space Reductions for LTL Model Checking of C and C++ ProgramsPetr Rockai, Jiri Barnat, Lubos Brim. 1-15 [doi]
- Regular Model Checking Using Solver Technologies and Automata LearningDaniel Neider, Nils Jansen. 16-31 [doi]
- Improved on-the-Fly Livelock DetectionAlfons Laarman, David Faragó. 32-47 [doi]
- Evaluating Human-Human Communication Protocols with Miscommunication Generation and Model CheckingMatthew L. Bolton, Ellen J. Bass. 48-62 [doi]
- Using Model-Checking to Reveal a Vulnerability of Tamper-Evident PairingRody Kersten, Bernard van Gastel, Manu Drijvers, Sjaak Smetsers, Marko C. J. D. van Eekelen. 63-77 [doi]
- SMT-Based Analysis of Biological ComputationBoyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi, Hillel Kugler. 78-92 [doi]
- Freshness and Reactivity Analysis in Globally Asynchronous Locally Time-Triggered SystemsFrédéric Boniol, Michaël Lauer, Claire Pagetti, Jérôme Ermont. 93-107 [doi]
- Enclosing Temporal Evolution of Dynamical Systems Using Numerical MethodsOlivier Bouissou, Alexandre Chapoutot, Adel Djoudi. 108-123 [doi]
- Inferring Automata with State-Local Alphabet AbstractionsMalte Isberner, Falk Howar, Bernhard Steffen. 124-138 [doi]
- Incremental Invariant Generation Using Logic-Based Automatic Abstract TransformersPierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli. 139-154 [doi]
- Numerical Abstract Domain Using Support FunctionsYassamine Seladji, Olivier Bouissou. 155-169 [doi]
- Widening as Abstract DomainBogdan Mihaila, Alexander Sepp, Axel Simon. 170-184 [doi]
- LiquidPi: Inferrable Dependent Session TypesDennis Griffith, Elsa L. Gunter. 185-197 [doi]
- Automated Verification of Chapel Programs Using Model Checking and Symbolic ExecutionTimothy K. Zirkel, Stephen F. Siegel, Timothy McClory. 198-212 [doi]
- Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-BoundingWei-Fan Chiang, Ganesh Gopalakrishnan, Guodong Li, Zvonimir Rakamaric. 213-228 [doi]
- Bounded Lazy InitializationJaco Geldenhuys, Nazareno Aguirre, Marcelo F. Frias, Willem Visser. 229-243 [doi]
- From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent SystemsDaniela Remenska, Jeff Templon, Tim A. C. Willemse, Philip Homburg, Kees Verstoep, Adria Casajus, Henri E. Bal. 244-260 [doi]
- Automatically Detecting Inconsistencies in Program SpecificationsAditi Tagore, Bruce W. Weide. 261-275 [doi]
- BLESS: Formal Specification and Verification of Behaviors for Embedded Systems with SoftwareBrian R. Larson, Patrice Chalin, John Hatcliff. 276-290 [doi]
- Towards Complete Specifications with an Error CalculusQuang Loc Le, Asankhaya Sharma, Florin Craciun, Wei-Ngan Chin. 291-306 [doi]
- A Probabilistic Quantitative Analysis of Probabilistic-Write/Copy-SelectChristel Baier, Benjamin Engel, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews, Marcus Völp. 307-321 [doi]
- Statistical Model Checking of Wireless Mesh Routing ProtocolsPeter Höfner, Annabelle McIver. 322-336 [doi]
- On-the-Fly Confluence Detection for Statistical Model CheckingArnd Hartmanns, Mark Timmer. 337-351 [doi]
- Optimizing Control Strategy Using Statistical Model CheckingAlexandre David, Dehui Du, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis. 352-367 [doi]
- Formal Stability Analysis of Optical ResonatorsUmair Siddique, Vincent Aravantinos, Sofiène Tahar. 368-382 [doi]
- Formal Verification of Nonlinear Inequalities with Taylor Interval ApproximationsAlexey Solovyev, Thomas C. Hales. 383-397 [doi]
- Verifying a Privacy CA Remote Attestation ProtocolBrigid Halling, Perry Alexander. 398-412 [doi]
- Formalization of Infinite Dimension Linear Spaces with Application to Quantum TheoryMohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar. 413-427 [doi]
- Formal Verification of a Parameterized Data Aggregation ProtocolSergio Feo Arenis, Bernd Westphal. 428-434 [doi]
- OnTrack: An Open Tooling Environment for Railway VerificationPhillip James, Matthew Trumble, Helen Treharne, Markus Roggenbach, Steve Schneider. 435-440 [doi]
- Verification of Numerical Programs: From Real Numbers to Floating Point NumbersAlwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson. 441-446 [doi]
- Extracting Hybrid Automata from Control CodeSteven Lyde, Matthew Might. 447-452 [doi]
- PyNuSMV: NuSMV as a Python LibrarySimon Busard, Charles Pecheur. 453-458 [doi]
- RV-Adding Runtime Verification to jUnitNormann Decker, Martin Leucker, Daniel Thoma. 459-464 [doi]
- Using Language Engineering to Lift Languages and Analyses at the Domain LevelDaniel Ratiu, Markus Völter, Bernd Kolb, Bernhard Schätz. 465-471 [doi]
- On Designing an ACL2-Based C Integer Type Safety Checking ToolKevin Krause, Jim Alves-Foss. 472-477 [doi]
- Hierarchical Safety CasesEwen Denney, Ganesh Pai, Iain Whiteside. 478-483 [doi]