FM 2016: 21ST INTERNATIONAL SYMPOSIUM ON FORMAL METHODS

A
Abdulla, Parosh Aziz	Counter-Example Guided Program Verification
Antonino, Pedro	Tighter Reachability Criteria for Deadlock-Freedom Analysis
Astefanoaei, Lacramioara	Compositional Parameter Synthesis
Atig, Mohamed Faouzi	Counter-Example Guided Program Verification
B
Bardin, Sébastien	Recovering high-level conditions from binary programs
Becker, Hanno	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Benes, Nikola	A Model Checking Approach to Discrete Bifurcation Analysis
Bensalem, Saddek	Local Planning of Multiparty Interactions with Bounded Horizons Compositional Parameter Synthesis
Biondi, Fabrizio	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
Bisgaard, Morten	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Bosnacki, Dragan	GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
Bozga, Marius	Local Planning of Multiparty Interactions with Bounded Horizons Compositional Parameter Synthesis
Brabrand, Claus	Finding Suitable Variability Abstractions for Family-Based Analysis
Brim, Lubos	A Model Checking Approach to Discrete Bifurcation Analysis
Broy, Manfred	A Logical Approach to Systems Engineering Artifacts: Semantic Relationships and Dependencies beyond Traceability - From Requirements to Functional and Architectural View
Böhm, Stanislav	State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
C
Cavada, Roberto	Model-Based Design of an Energy-System Embedded Controller using Taste
Chand, Saksham	Formal Verification of Multi-Paxos for Distributed Consensus
Chen, Mingshuai	Validated Simulation-Based Verification of Delayed Differential Dynamics
Chen, Xiaohong	Towards Concolic Testing for Hybrid Systems
Chen, Xin	A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Chen, Yuqi	Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Cheng, Chih-Hong	Compositional Parameter Synthesis
Chifflier, Pierre	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Chin, Wei-Ngan	Automated Mutual Explicit Induction Proof in Separation Logic
Cimatti, Alessandro	Model-Based Design of an Energy-System Embedded Controller using Taste From Electrical Switched Networks to Hybrid Automata
Colvin, Robert	An algebra of synchronous atomic steps
Combaz, Jacques	Local Planning of Multiparty Interactions with Bounded Horizons
Crema, Luigi	Model-Based Design of an Energy-System Embedded Controller using Taste
Crespo, Juan Manuel	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
D
David, Cristina	Danger Invariants
Day, Nancy	Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Dellabani, Mahieddine	Local Planning of Multiparty Interactions with Bounded Horizons
Demko, Martin	A Model Checking Approach to Discrete Bifurcation Analysis
Diep, Bui Phi	Counter-Example Guided Program Verification
Dimovski, Aleksandar S.	Finding Suitable Variability Abstractions for Family-Based Analysis
Djoudi, Adel	Recovering high-level conditions from binary programs
Dong, Jin Song	Automated Verification of Timed Security Protocols with Clock Drift
F
Feyling, Claus	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
Filipovikj, Predrag	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Flores Montoya, Antonio E.	Upper and Lower Amortized Cost Bounds of Programs Expressed as Cost Relations
Fränzle, Martin	Discounted Duration Calculus Validated Simulation-Based Verification of Delayed Differential Dynamics
G
Galowicz, Jacek	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Gerhardt, David	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Ghezzi, Carlo	Dealing with Incompleteness in Automata-based Model Checking
Ghorbal, Khalil	Decoupled simulating abstractions of non-linear ordinary differential equations
Giannakopoulou, Dimitra	Exploring Model Quality for ACAS X
Giantamidis, Georgios	Learning Moore Machines from Input-Output Traces
Gibson-Robinson, Thomas	Tighter Reachability Criteria for Deadlock-Freedom Analysis
Gomes, Victor B. F.	Modal Kleene Algebra Applied to Program Correctness
Gotsman, Alexey	A Generic Logic for Proving Linearizability
Goubault, Éric	Recovering high-level conditions from binary programs
Griesmayer, Andreas	Equivalence Checking of a Floating-point Unit Against a High-level C Model
Grov, Gudmund	Mechanised Verification Patterns for Dafny
Grumberg, Orna	Sound and Complete Mutation-Based Program Repair
Gu, Ming	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Guck, Dennis	Exploring Model Quality for ACAS X
H
Hansen, Michael R.	Discounted Duration Calculus
Hasanagic, Miran	Formalising and Validating the Interface Description in the FMI standard
Hayes, Ian J.	An algebra of synchronous atomic steps
Hensel, Ulrich	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Hermanns, Holger	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Hiet, Guillaume	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Hirai, Yoichi	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Hoa, Koh Chuen	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Hofmann, Martin	An Implementation of Deflate in Coq
Holzer, Andreas	Error Invariants for Concurrent Traces
Honiden, Shinichi	Refactoring Refinement Structures of Event-B Machines
Hou, Zhe	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Huang, Chao	A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Huang, Wen-Ling	Industrial-strength Model-based Testing of Safety-critical Systems
I
Ipate, Florentin	RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
Ishikawa, Fuyuki	Refactoring Refinement Structures of Event-B Machines
J
Jancar, Petr	State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Jiang, Yu	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Jiao, Li	Approximate Bisimulation and Discretization of Hybrid CSP
Johansen, Christian	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
Johnson, Taylor T	Decoupled simulating abstractions of non-linear ordinary differential equations
Joshi, Saurabh	Equivalence Checking of a Floating-point Unit Against a High-level C Model
K
Kawamoto, Yusuke	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
Kesseli, Pascal	Danger Invariants
Khoo, Siau-Cheng	Automated Mutual Explicit Induction Proof in Separation Logic
Khyzha, Artem	A Generic Logic for Proving Linearizability
Kobayashi, Tsutomu	Refactoring Refinement Structures of Event-B Machines
Kong, Hui	Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Kong, Pingfan	Towards Concolic Testing for Hybrid Systems
Kroening, Daniel	Equivalence Checking of a Floating-point Unit Against a High-level C Model Danger Invariants
Krčál, Jan	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Kunz, César	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
L
Lahav, Ori	Explaining Relaxed Memory Models with Program Transformations
Larsen, Peter Gorm	Formalising and Validating the Interface Description in the FMI standard
Lausdahl, Kenneth	Formalising and Validating the Interface Description in the FMI standard
Le, Ton Chanh	Automated Mutual Explicit Induction Proof in Separation Logic
Legay, Axel	Hybrid Statistical Estimation of Mutual Information for Quantifying Information Flow
Letan, Thomas	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Lewis, Matt	Danger Invariants
Li, Li	Automated Verification of Timed Security Protocols with Clock Drift
Li, Yangjia	Validated Simulation-Based Verification of Delayed Differential Dynamics Approximate Bisimulation and Discretization of Hybrid CSP
Li, Yi	Towards Concolic Testing for Hybrid Systems
Lin, Wang	A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Lin, Yuhui	Mechanised Verification Patterns for Dafny
Liu, Annie	Formal Verification of Multi-Paxos for Distributed Consensus
Liu, Han	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Liu, Yang	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Liu, Zhiming	A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Ljungkrantz, Oscar	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Luteberget, Bjørnar	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
Lönn, Henrik	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
M
Mahmud, Nesredin	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Marinescu, Raluca	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Meca, Ondřej	State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI
Meinicke, Larissa	An algebra of synchronous atomic steps
Melham, Tom	Equivalence Checking of a Floating-point Unit Against a High-level C Model
Menghi, Claudio	Dealing with Incompleteness in Automata-based Model Checking
Morin, Benjamin	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
Mosaad, Peter N.	Validated Simulation-Based Verification of Delayed Differential Dynamics
Mover, Sergio	From Electrical Switched Networks to Hybrid Automata
Mukherjee, Rajdeep	Equivalence Checking of a Floating-point Unit Against a High-level C Model
N
Nakata, Keiko	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Neele, Thomas	GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
Nies, Gilles	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Néron, Pierre	SpecCert: Specifying and Verifying Hardware-based Security Enforcement
O
O'Hearn, Peter	Moving Fast with Program Verification Technology
Ody, Heinrich	Discounted Duration Calculus
P
Parkinson, Matthew	A Generic Logic for Proving Linearizability
Pastva, Samuel	A Model Checking Approach to Discrete Bifurcation Analysis
Peleska, Jan	Industrial-strength Model-based Testing of Safety-critical Systems
Poskitt, Christopher M.	Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Predut, Sorina	RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
R
Roccabruna, Mattia	Model-Based Design of an Energy-System Embedded Controller using Taste
Roscoe, Bill	Tighter Reachability Criteria for Deadlock-Freedom Analysis
Rothenberg, Bat-Chen	Sound and Complete Mutation-Based Program Repair
Ruess, Harald	Compositional Parameter Synthesis
S
Sacchini, Jorge Luis	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Sanan, David	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Schumann, Johann	Exploring Model Quality for ACAS X
Schwartz-Narbonne, Daniel	Error Invariants for Concurrent Traces
Seceleanu, Cristina	Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems
Senjak, Christoph-Simon	An Implementation of Deflate in Coq
Sessa, Mirko	From Electrical Switched Networks to Hybrid Automata
Sha, Lui	Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Sogokon, Andrew	Decoupled simulating abstractions of non-linear ordinary differential equations
Song, Houbing	Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Spoletini, Paola	Dealing with Incompleteness in Automata-based Model Checking
Stefanescu, Alin	RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
Steffen, Martin	Rule-based Incremental Verification Tools Applied to Railway Designs and Regulations
Stenger, Marvin	Battery-Aware Scheduling in Low Orbit: The GomX-3 Case
Stoenescu, Teodor	RIVER: A Binary Analysis Framework using Symbolic Execution and Reversible x86 Instructions
Stoller, Scott	Formal Verification of Multi-Paxos for Distributed Consensus
Strichman, Ofer	Regression Verification for unbalanced recursive functions
Struth, Georg	Modal Kleene Algebra Applied to Program Correctness
Sun, Jiaguang	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers Safety-Assured Formal Model-Driven Design of the Multifunction Vehicle Bus Controller
Sun, Jun	Towards Concolic Testing for Hybrid Systems Automated Verification of Timed Security Protocols with Clock Drift Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation
Sun, Meng	Towards Concolic Testing for Hybrid Systems
T
Ta, Quang-Trung	Automated Mutual Explicit Induction Proof in Separation Logic
Tabaei Befrouei, Mitra	Error Invariants for Concurrent Traces
Tews, Hendrik	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Tiu, Alwen	An Executable Formalisation of the SPARCv8 Instruction Set Architecture: A Case Study for The LEON3 Processor
Tonetta, Stefano	Model-Based Design of an Energy-System Embedded Controller using Taste
Tripakis, Stavros	Learning Moore Machines from Input-Output Traces
Tuerk, Thomas	Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
Tumas, Vytautas	Mechanised Verification Patterns for Dafny
V
Vafeiadis, Viktor	Explaining Relaxed Memory Models with Program Transformations
Vakili, Amirhossein	Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Veitsman, Maor	Regression Verification for unbalanced recursive functions
Velykis, Andrius	An algebra of synchronous atomic steps
W
W. V. Tran-Jørgensen, Peter	Formalising and Validating the Interface Description in the FMI standard
Wang, Jingyi	Towards Concolic Testing for Hybrid Systems
Wang, Shuling	Approximate Bisimulation and Discretization of Hybrid CSP
Wasowski, Andrzej	Finding Suitable Variability Abstractions for Family-Based Analysis
Weissenbacher, Georg	Error Invariants for Concurrent Traces
Wies, Thomas	Error Invariants for Concurrent Traces
Wijs, Anton	GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
Winter, Kirsten	An algebra of synchronous atomic steps
Y
Yan, Gaogao	Approximate Bisimulation and Discretization of Hybrid CSP
Yang, Zhengfeng	A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems
Z
Zhan, Naijun	Validated Simulation-Based Verification of Delayed Differential Dynamics Approximate Bisimulation and Discretization of Hybrid CSP
Zhang, Huafeng	Taming Interrupts For Verifying Industrial Multifunction Vehicle Bus Controllers
Š
Šafránek, David	A Model Checking Approach to Discrete Bifurcation Analysis

Disclaimer | Powered by EasyChair Smart Program