FM 2015: FORMAL METHODS 2015

A
Abdelkader, Karam	Automated Circular Assume-Guarantee Reasoning
Abraham, Erika	Counterexamples for Expected Rewards
Ahrendt, Wolfgang	A Specification Language for Static and Runtime Verification of Data and Control Properties
Albert, Elvira	Resource Analysis: From Sequential to Concurrent and Distributed Programs
Alturki, Musab A.	Towards Formal Verification of Orchestration Computations Using the K Framework
Alzuhaibi, Omar	Towards Formal Verification of Orchestration Computations Using the K Framework
Amato, Gianluca	Narrowing operators on template abstract domains
Andronick, June	Automated Verification of RPC Stub Code
Araki, Keijiro	Practices for Formal Models as Documents: Evolution of VDM Application to ``Mobile FeliCa" IC Chip Firmware
B
Bagheri, Hamid	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
Becker, Bernd	Counterexamples for Expected Rewards
Biallas, Sebastian	Analyzing the Restart Behavior of Industrial Control Applications
Brat, Guillaume	Verifying the Safety of a Flight-Critical System
Bringer, Julien	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Bushnell, David	Verifying the Safety of a Flight-Critical System
C
Carle, Georg	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Chabanne, Hervé	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Chauhan, Avriti	Eliminating Static Analysis False Positives using Loop Abstraction and Bounded Model Checking
Chavda, Anooj	Eliminating Static Analysis False Positives using Loop Abstraction and Bounded Model Checking
Chimdyalwar, Bharti	Eliminating Static Analysis False Positives using Loop Abstraction and Bounded Model Checking
Chimento, Jesus Mauricio	A Specification Language for Static and Runtime Verification of Data and Control Properties
Chin, Wei-Ngan	Certified Reasoning with Infinity
Conchon, Sylvain	Certificates for Parameterized Model Checking
Costea, Andreea	Certified Reasoning with Infinity
D
Damm, Werner	AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned
Dang, Thao	Parameter Synthesis through Temporal Logic Specifications
Darke, Priyanka	Eliminating Static Analysis False Positives using Loop Abstraction and Bounded Model Checking
Davies, Misty	Verifying the Safety of a Flight-Critical System
Debois, Søren	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
Dehnert, Christian	Counterexamples for Expected Rewards
Derrick, John	Verifying Opacity of a Transactional Mutex Lock A framework for correctness criteria on weak memory models
Di Nardo Di Maio, Simone	Narrowing operators on template abstract domains
Diekmann, Cornelius	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Diskin, Zinovy	The Semantics of Cardinality-based Feature Models via Formal Languages
Dong, Jin Song	Verifying Parameterized Timed Security Protocols
Dongol, Brijesh	Verifying Opacity of a Transactional Mutex Lock
Dreossi, Tommaso	Parameter Synthesis through Temporal Logic Specifications
Du, Xiaoning	Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
Durand, William	Autofunk: an inference-based formal model generation framework for production systems.
E
Eisentraut, Christian	Probabilistic Bisimulation for Realistic Schedulers
Evans, Neil	Software Development and Authentication for Arms Control Information Barriers
F
Feng, Yuan	QPMC: A Model Checker for Quantum Programs and Protocols
Ferguson, Andrew D.	Static Differential Program Analysis for Software-Defined Networks
Fernandez, Matthew	Automated Verification of RPC Stub Code
Furia, Carlo A.	A Fully Verified Container Library
G
Giannakopoulou, Dimitra	Verifying the Safety of a Flight-Critical System
Godskesen, Jens Chr.	Probabilistic Bisimulation for Realistic Schedulers
Gopalakrishnan, Ganesh	Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Grumberg, Orna	Automated Circular Assume-Guarantee Reasoning
Gu, Yu-Lei	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
H
Hahn, Ernst Moritz	QPMC: A Model Checker for Quantum Programs and Protocols
Hauck-Stattelmann, Stefan	Analyzing the Restart Behavior of Industrial Control Applications
Hermanns, Holger	Probabilistic Bisimulation for Realistic Schedulers
Hildebrandt, Thomas	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
Hobor, Aquinas	Certified Reasoning with Infinity
Hooman, Jozef	Formalizing the Concept Phase of Product Development at Philips Healthcare
Howar, Falk	Verifying the Safety of a Flight-Critical System
Hupel, Lars	Semantics-Preserving Simplification of Real-World Firewall Rule Sets
Huuck, Ralf	Case Study: Static Security Analysis of the Android Goldfish Kernel
I
Ishikawa, Fuyuki	Practices for Formal Models as Documents: Evolution of VDM Application to ``Mobile FeliCa" IC Chip Firmware
Issarny, Valerie	The key role of formal methods to overcome the interoperability challenge.
J
Jackson, Daniel	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
Jackson, Paul	Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Jacobsen, Charlie	Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Jansen, Nils	Counterexamples for Expected Rewards
Jetley, Raoul	Analyzing the Restart Behavior of Industrial Control Applications
Joshi, Saurabh	Property-Driven Fence Insertion using Reorder Bounded Model Checking
K
Kahsai, Temesghen	Verifying the Safety of a Flight-Critical System
Kang, Eunsuk	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
Katoen, Joost-Pieter	Counterexamples for Expected Rewards
Klein, Gerwin	Automated Verification of RPC Stub Code
Kowalewski, Stefan	Analyzing the Restart Behavior of Industrial Control Applications
Krishnamurthi, Shriram	Static Differential Program Analysis for Software-Defined Networks
Kroening, Daniel	Proving Safety with Trace Automata and Bounded Model Checking Property-Driven Fence Insertion using Reorder Bounded Model Checking
Kurita, Taro	Practices for Formal Models as Documents: Evolution of VDM Application to ``Mobile FeliCa" IC Chip Firmware
Kuz, Ihor	Automated Verification of RPC Stub Code
L
Lamport, Leslie	What Should Math Have to do with Building Complex Distributed Systems?
Le Métayer, Daniel	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Lecomte, Thierry	Formal Virtual Modelling and Data Verification for Supervision Systems
Lescuyer, Roch	Privacy by design in practice: reasoning about privacy properties of biometric system architectures
Leuschel, Michael	Model-Based Problem Solving for University Timetable Validation and Improvement
Lewis, Matt	Proving Safety with Trace Automata and Bounded Model Checking
Li, Li	Verifying Parameterized Timed Security Protocols
Liu, Jiang	Abstraction of Elementary Hybrid Systems by Variable Transformation
Liu, Tao	Case Study: Static Security Analysis of the Android Goldfish Kernel
Liu, Yang	Verifying Parameterized Timed Security Protocols Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
M
Maibaum, Tom	The Semantics of Cardinality-based Feature Models via Formal Languages
Malek, Sam	Detection of Design Flaws in the Android Permission Protocol through Bounded Verification
Masini, Henrique	Using Simulink Design Verifier for Automatic Generation of Requirements-based Tests
Mebsout, Alain	Certificates for Parameterized Model Checking
Meo, Maria Chiara	Narrowing operators on template abstract domains
Miranda, Bruno	Using Simulink Design Verifier for Automatic Generation of Requirements-based Tests
N
Nakajima, Shin	Using Real-Time Maude to Model Check Energy Consumption Behavior
Nelson, Tim	Static Differential Program Analysis for Software-Defined Networks
P
Pace, Gordon	A Specification Language for Static and Runtime Verification of Data and Control Properties
Pasareanu, Corina	Automated Circular Assume-Guarantee Reasoning
Piazza, Carla	Parameter Synthesis through Temporal Logic Specifications
Polikarpova, Nadia	A Fully Verified Container Library
Q
Quatmann, Tim	Counterexamples for Expected Rewards
R
Rakamaric, Zvonimir	Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Reis, Rodrigo	Using Simulink Design Verifier for Automatic Generation of Requirements-based Tests
S
Safilian, Aliakbar	The Semantics of Cardinality-based Feature Models via Formal Languages
Salva, Sébastien	Autofunk: an inference-based formal model generation framework for production systems.
Schellhorn, Gerhard	Verifying Opacity of a Transactional Mutex Lock
Schlich, Bastian	Analyzing the Restart Behavior of Industrial Control Applications
Schmitt, Peter	Typed First-Order Logic
Schneider, David	Model-Based Problem Solving for University Timetable Validation and Improvement
Schneider, Gerardo	A Specification Language for Static and Runtime Verification of Data and Control Properties
Schuts, Mathijs	Formalizing the Concept Phase of Product Development at Philips Healthcare
Scozzari, Francesca	Narrowing operators on template abstract domains
Sharma, Asankhaya	Certified Reasoning with Infinity
Shoham, Sharon	Automated Circular Assume-Guarantee Reasoning
Slaats, Tijs	Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes
Smith, Graeme	A framework for correctness criteria on weak memory models
Sogokon, Andrew	Direct formal verification of liveness properties in continuous and hybrid dynamical systems
Solovyev, Alexey	Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Song, Lei	Probabilistic Bisimulation for Realistic Schedulers
Sun, Jun	Verifying Parameterized Timed Security Protocols
T
Tiu, Alwen	Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL
Travkin, Oleg	Verifying Opacity of a Transactional Mutex Lock
Tschannen, Julian	A Fully Verified Container Library
Turrini, Andrea	QPMC: A Model Checker for Quantum Programs and Protocols
U
Ulbrich, Mattias	Typed First-Order Logic
V
Vaghani, Sagar	Eliminating Static Analysis False Positives using Loop Abstraction and Bounded Model Checking
W
Wang, Shengyi	Certified Reasoning with Infinity
Wehrheim, Heike	Verifying Opacity of a Transactional Mutex Lock
Weissenbacher, Georg	Proving Safety with Trace Automata and Bounded Model Checking
Wimmer, Ralf	Counterexamples for Expected Rewards
Witt, Tobias	Model-Based Problem Solving for University Timetable Validation and Improvement
Y
Yan, Rongjie	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Z
Zaidi, Fatiha	Certificates for Parameterized Model Checking
Zhan, Naijun	Abstraction of Elementary Hybrid Systems by Variable Transformation
Zhang, Guangquan	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Zhang, Jian	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Zhang, Lijun	Probabilistic Bisimulation for Realistic Schedulers QPMC: A Model Checker for Quantum Programs and Protocols
Zhang, Wenhui	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Zhao, Hengjun	Abstraction of Elementary Hybrid Systems by Variable Transformation
Zhu, Xue-Yang	Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking
Zou, Liang	Abstraction of Elementary Hybrid Systems by Variable Transformation

Disclaimer | Powered by EasyChair Smart Program