Automated Verification of Timed Security Protocols with Clock Drift
Modal Kleene Algebra Applied to Program Correctness
Antonio E. Flores Montoya.
Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
An algebra of synchronous atomic steps
Zhe Hou, David Sanan, Alwen Tiu, Yang Liu and Koh Chuen Hoa.
An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
A Model Checking Approach to Discrete Bifurcation Analysis
Local Planning of Multiparty Interactions with a Bounded Horizon
Recovering high-level conditions from binary programs
SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Exploring Model Quality for ACAS X
Equivalence Checking of a Floating-point Unit Against a High-level C Model
Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
Sound and Complete Mutation-Based Program Repair
Formalising and Validating the Interface Description in the FMI standard
A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Regression Verification for unbalanced recursive functions
Approximate Bisimulation and Discretization of Hybrid CSP
Refactoring Refinement Structures of Event-B Machines
Towards Concolic Testing for Hybrid Systems
Validated Simulation-Based Verification of Delayed Differential Dynamics
Automated Mutual Explicit Induction Proof in Separation Logic
State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
An Implementation of Deflate in Coq
Mechanised Verification Patterns for Dafny
Discounted Duration Calculus
Compositional Parameter Synthesis
Explaining Relaxed Memory Models with Program Transformations
Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Formal Verification of Multi-Paxos for Distributed Consensus
Finding Suitable Variability Abstractions for Family-Based Analysis
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
Tighter Reachability Criteria for Deadlock-Freedom Analysis
Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
From Electrical Switched Networks to Hybrid Automata
Dealing with Incompleteness in Automata-based Model Checking
Counter-Example Guided Program Verification
Decoupled simulating abstractions of non-linear ordinary differential equations
Learning Moore Machines from Input-Output Traces
Error Invariants for Concurrent Traces
Teodor Stoenescu, Alin Stefanescu, Sorina Predut and Florentin Ipate.
RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
Roberto Cavada, Alessandro Cimatti, Luigi Crema, Mattia Roccabruna and Stefano Tonetta.
Model-Based Design of an Energy-System Embedded Controller using Taste
Bjørnar Luteberget, Christian Johansen, Claus Feyling and Martin Steffen.
Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
Han Liu, Yu Jiang, Huafeng Zhang, Ming Gu and Jiaguang Sun.
Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers
Predrag Filipovikj, Nesredin Mahmud, Raluca Marinescu, Cristina Seceleanu, Oscar Ljungkrantz and Henrik Lönn.
Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Yu Jiang, Han Liu, Hui Kong, Houbing Song, Ming Gu, Jiaguang Sun and Lui Sha.
Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Model-Based Database Design
Mechanising the Translation from Circus to CSPm or Model-Checking Circus
Verifying the Co-Simulation Orchestration Engine for INTO-CPS
Hardware Verification Using Software Analyzers
Saulo Rodrigues E Silva.
Efficient development of models for user interfaces in high assurance systems
Parallel Model Checking of ω-Automata
Risk Assessment in Collaborative Robotic
Quality analysis and verification of data-intensive applications