Abstract is missing.
- Industrial-Strength Model-Based Testing of Safety-Critical SystemsJan Peleska, Wen-ling Huang. 3-22 [doi]
- Counter-Example Guided Program VerificationParosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep. 25-42 [doi]
- Tighter Reachability Criteria for Deadlock-Freedom AnalysisPedro R. G. Antonino, Thomas Gibson-Robinson, A. W. Roscoe. 43-59 [doi]
- Compositional Parameter SynthesisLacramioara Astefanoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess. 60-68 [doi]
- Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a HypervisorHanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk. 69-84 [doi]
- A Model Checking Approach to Discrete Bifurcation AnalysisNikola Benes, Lubos Brim, Martin Demko, Samuel Pastva, David Safránek. 85-101 [doi]
- State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPIStanislav Böhm, Ondrej Meca, Petr Jancar. 102-118 [doi]
- Formal Verification of Multi-Paxos for Distributed ConsensusSaksham Chand, Yanhong A. Liu, Scott D. Stoller. 119-136 [doi]
- Validated Simulation-Based Verification of Delayed Differential DynamicsMingshuai Chen, Martin Fränzle, Yangjia Li, Peter Nazier Mosaad, Naijun Zhan. 137-154 [doi]
- Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code MutationYuqi Chen, Christopher M. Poskitt, Jun Sun 0001. 155-163 [doi]
- From Electrical Switched Networks to Hybrid AutomataAlessandro Cimatti, Sergio Mover, Mirko Sessa. 164-181 [doi]
- Danger InvariantsCristina David, Pascal Kesseli, Daniel Kroening, Matt Lewis. 182-198 [doi]
- Local Planning of Multiparty Interactions with Bounded HorizonsMahieddine Dellabani, Jacques Combaz, Marius Bozga, Saddek Bensalem. 199-216 [doi]
- Finding Suitable Variability Abstractions for Family-Based AnalysisAleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski. 217-234 [doi]
- Recovering High-Level Conditions from Binary ProgramsAdel Djoudi, Sébastien Bardin, Éric Goubault. 235-253 [doi]
- Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost RelationsAntonio Flores-Montoya. 254-273 [doi]
- Exploring Model Quality for ACAS XDimitra Giannakopoulou, Dennis Guck, Johann Schumann. 274-290 [doi]
- Learning Moore Machines from Input-Output TracesGeorgios Giantamidis, Stavros Tripakis. 291-309 [doi]
- Modal Kleene Algebra Applied to Program CorrectnessVictor B. F. Gomes, Georg Struth. 310-325 [doi]
- Mechanised Verification Patterns for DafnyGudmund Grov, Yuhui Lin, Vytautas Tumas. 326-343 [doi]
- Formalising and Validating the Interface Description in the FMI StandardMiran Hasanagic, Peter W. V. Tran-Jørgensen, Kenneth Lausdahl, Peter Gorm Larsen. 344-351 [doi]
- An Algebra of Synchronous Atomic StepsIan J. Hayes, Robert J. Colvin, Larissa A. Meinicke, Kirsten Winter, Andrius Velykis. 352-369 [doi]
- Error Invariants for Concurrent TracesAndreas Holzer, Daniel Schwartz-Narbonne, Mitra Tabaei Befrouei, Georg Weissenbacher, Thomas Wies. 370-387 [doi]
- An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for the LEON3 ProcessorZhe Hou, David Sanán, Alwen Tiu, Yang Liu, Koh Chuen Hoa. 388-405 [doi]
- Hybrid Statistical Estimation of Mutual Information for Quantifying Information FlowYusuke Kawamoto, Fabrizio Biondi, Axel Legay. 406-425 [doi]
- A Generic Logic for Proving LinearizabilityArtem Khyzha, Alexey Gotsman, Matthew J. Parkinson. 426-443 [doi]
- Refactoring Refinement Structure of Event-B MachinesTsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden. 444-459 [doi]
- Towards Concolic Testing for Hybrid SystemsPingfan Kong, Yi Li, Xiaohong Chen, Jun Sun 0001, Meng Sun, Jingyi Wang. 460-478 [doi]
- Explaining Relaxed Memory Models with Program TransformationsOri Lahav, Viktor Vafeiadis. 479-495 [doi]
- SpecCert: Specifying and Verifying Hardware-Based Security EnforcementThomas Letan, Pierre Chifflier, Guillaume Hiet, Pierre Néron, Benjamin Morin. 496-512 [doi]
- Automated Verification of Timed Security Protocols with Clock DriftLi Li, Jun Sun 0001, Jin Song Dong. 513-530 [doi]
- Dealing with Incompleteness in Automata-Based Model CheckingClaudio Menghi, Paola Spoletini, Carlo Ghezzi. 531-550 [doi]
- Equivalence Checking of a Floating-Point Unit Against a High-Level C ModelRajdeep Mukherjee, Saurabh Joshi 0001, Andreas Griesmayer, Daniel Kroening, Tom Melham. 551-558 [doi]
- Battery-Aware Scheduling in Low Orbit: The GomX-3 CaseMorten Bisgaard, David Gerhardt, Holger Hermanns, Jan Krcál, Gilles Nies, Marvin Stenger. 559-576 [doi]
- Discounted Duration CalculusHeinrich Ody, Martin Fränzle, Michael R. Hansen. 577-592 [doi]
- Sound and Complete Mutation-Based Program RepairBat-Chen Rothenberg, Orna Grumberg. 593-611 [doi]
- An Implementation of Deflate in CoqChristoph-Simon Senjak, Martin Hofmann. 612-627 [doi]
- Decoupling Abstractions of Non-linear Ordinary Differential EquationsAndrew Sogokon, Khalil Ghorbal, Taylor T. Johnson. 628-644 [doi]
- Regression Verification for Unbalanced Recursive FunctionsOfer Strichman, Maor Veitsman. 645-658 [doi]
- Automated Mutual Explicit Induction Proof in Separation LogicQuang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin. 659-676 [doi]
- Finite Model Finding Using the Logic of Equality with Uninterpreted FunctionsAmirhossein Vakili, Nancy A. Day. 677-693 [doi]
- GPUexplore 2.0: Unleashing GPU Explicit-State Model CheckingAnton Wijs, Thomas Neele, Dragan Bosnacki. 694-701 [doi]
- Approximate Bisimulation and Discretization of Hybrid CSPGaogao Yan, Li Jiao, Yangjia Li, Shuling Wang, Naijun Zhan. 702-720 [doi]
- A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid SystemsZhengfeng Yang, Chao Huang, Xin Chen, Wang Lin, Zhiming Liu 0001. 721-738 [doi]
- Model-Based Design of an Energy-System Embedded Controller Using TasteRoberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna, Stefano Tonetta. 741-747 [doi]
- Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial SystemsPredrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz, Henrik Lönn. 748-756 [doi]
- Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus ControllerYu Jiang, Han Liu, Houbing Song, Hui Kong, Ming Gu, Jiaguang Sun, Lui Sha. 757-763 [doi]
- Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus ControllersHan Liu, Yu Jiang, Huafeng Zhang, Ming Gu, Jiaguang Sun. 764-771 [doi]
- Rule-Based Incremental Verification Tools Applied to Railway Designs and RegulationsBjørnar Luteberget, Christian Johansen, Claus Feyling, Martin Steffen. 772-778 [doi]
- RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 InstructionsTeodor Stoenescu, Alin Stefanescu, Sorina Predut, Florentin Ipate. 779-785 [doi]