Abstract is missing.
- DO-333 Certification Case StudiesDarren D. Cofer, Steven M. Miller. 1-15 [doi]
- A Compositional Monitoring Framework for Hard Real-Time SystemsAndré de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto. 16-30 [doi]
- Leadership Election: An Industrial SoS Application of Compositional Deadlock VerificationPedro R. G. Antonino, Marcel Medeiros Oliveira, Augusto C. A. Sampaio, Klaus E. Kristensen, Jeremy W. Bryans. 31-45 [doi]
- Verification of Certifying Computations through AutoCorres and SimplLars Noschinski, Christine Rizkallah, Kurt Mehlhorn. 46-61 [doi]
- Distinguishing Sequences for Partially Specified FSMsRobert M. Hierons, Uraz Cengiz Türker. 62-76 [doi]
- On Proving Recoverability of Smart Electrical GridsSeppo Horsmanheimo, Maryam Kamali, Mikko Kolehmainen, Mats Neovius, Luigia Petre, Mauno Rönkkö, Petter Sandvik. 77-91 [doi]
- Providing Early Warnings of Specification ProblemsDustin Hoffman, Aditi Tagore, Diego Zaccai, Bruce W. Weide. 92-97 [doi]
- Mechanized, Compositional Verification of Low-Level CodeBjörn Bartels, Nils Jähnig. 98-112 [doi]
- Formally Verified Computation of Enclosures of Solutions of Ordinary Differential EquationsFabian Immler. 113-127 [doi]
- On the Quantum Formalization of Coherent Light in HOLMohamed Yousri Mahmoud, Sofiène Tahar. 128-142 [doi]
- Refinement Types for tla +Stephan Merz, Hernán Vanzetto. 143-157 [doi]
- Using Lightweight Theorem Proving in an Asynchronous Systems ContextMatthew Danish, Hongwei Xi. 158-172 [doi]
- JKelloy: A Proof Assistant for Relational Specifications of Java ProgramsAboubakr Achraf El Ghazi, Mattias Ulbrich, Christoph Gladisch, Shmuel S. Tyszberowicz, Mana Taghdiri. 173-187 [doi]
- Verifying Hybrid Systems Involving Transcendental FunctionsPaul Jackson, Andrew Sogokon, James P. Bridge, Lawrence C. Paulson. 188-202 [doi]
- Verifying Nonpolynomial Hybrid Systems by Qualitative Abstraction and Automated Theorem ProvingWilliam Denman. 203-208 [doi]
- Combining PVSio with StateflowPaolo Masci, Yi Zhang, Paul L. Jones, Patrick Oladimeji, Enrico D'Urso, Cinzia Bernardeschi, Paul Curzon, Harold Thimbleby. 209-214 [doi]
- Qed. Computing What Remains to Be ProvedLoïc Correnson. 215-229 [doi]
- Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU KernelsEthel Bardsley, Alastair F. Donaldson. 230-245 [doi]
- Testing-Based Compiler Validation for Synchronous LanguagesPierre-Loïc Garoche, Falk Howar, Temesghen Kahsai, Xavier Thirioux. 246-251 [doi]
- Automated Testcase Generation for Numerical Support Functions in Embedded SystemsJohann Schumann, Stefan-Alexander Schneider. 252-257 [doi]
- REFINER: Towards Formal Verification of Model TransformationsAnton Wijs, Luc Engelen. 258-263 [doi]
- Designing a Deadlock-Free Train Scheduler: A Model Checking ApproachFranco Mazzanti, Giorgio Oronzo Spagnolo, Alessio Ferrari. 264-269 [doi]
- A Synthesized Algorithm for Interactive ConsistencyAdria Gascón, Ashish Tiwari. 270-284 [doi]
- Energy-Utility QuantilesChristel Baier, Marcus Daum, Clemens Dubslaff, Joachim Klein, Sascha Klüppelholz. 285-299 [doi]
- Incremental Verification of Compiler OptimizationsGrigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina. 300-306 [doi]
- Memory Efficient Data Structures for Explicit Verification of Timed SystemsPeter Gjøl Jensen, Kim Guldstrand Larsen, Jirí Srba, Mathias Grund Sørensen, Jakob Haahr Taankvist. 307-312 [doi]
- The Gradual VerifierStephan Arlt, Cindy Rubio-González, Philipp Rümmer, Martin Schäf, Natarajan Shankar. 313-327 [doi]
- Synthesizing Predicates from Abstract Domain LossesBogdan Mihaila, Axel Simon. 328-342 [doi]
- Formal Verification of kLIBC with the WP Frama-C Plug-inNuno Carvalho, Cristiano da Silva Sousa, Jorge Sousa Pinto, Aaron Tomb. 343-358 [doi]