FM 2015: FORMAL METHODS 2015
PROGRAM

Days: Wednesday, June 24th Thursday, June 25th Friday, June 26th

Wednesday, June 24th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 1: Keynote
Location: Simula
09:00
Resource Analysis: From Sequential to Concurrent and Distributed Programs (abstract)
10:30-12:30 Session 2A: Probabilistic and Hybrid Systems
Location: Smalltalk
10:30
Direct formal verification of liveness properties in continuous and hybrid dynamical systems (abstract)
11:00
Counterexamples for Expected Rewards (abstract)
11:30
Probabilistic Bisimulation for Realistic Schedulers (abstract)
12:00
Abstraction of Elementary Hybrid Systems by Variable Transformation (abstract)
10:30-12:30 Session 2B: Security
Location: Simula
10:30
Certified Reasoning with Infinity (abstract)
11:00
Detection of Design Flaws in the Android Permission Protocol through Bounded Verification (abstract)
11:30
Privacy by design in practice: reasoning about privacy properties of biometric system architectures (abstract)
12:00
Verifying Parameterized Timed Security Protocols (abstract)
14:00-15:30 Session 3A: Temporal Logic
Location: Smalltalk
14:00
Using Real-Time Maude to Model Check Energy Consumption Behavior (abstract)
14:30
Trace-Length Independent Runtime Monitoring of Quantitative Policies in LTL (abstract)
15:00
Parameter Synthesis through Temporal Logic Specifications (abstract)
14:00-15:30 Session 3B: Model Checking and Runtime Verification
Location: Simula
14:00
Verifying the Safety of a Flight-Critical System (abstract)
14:30
A Specification Language for Static and Runtime Verification of Data and Control Properties (abstract)
15:00
Safety, Liveness and Run-time Refinement for Modular Process-Aware Information Systems with Dynamic Sub Processes (abstract)
16:00-17:00 Session 4: Keynote
Location: Simula
16:00
What Should Math Have to do with Building Complex Distributed Systems? (abstract)
Thursday, June 25th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 5: Keynote
Location: Simula
09:00
AVACS: Automatic Verification and Analysis of Complex Systems Highlights and Lessons Learned (abstract)
10:30-12:30 Session 6A: Case Studies: Verification in Practice
Location: Simula
10:30
Semantics-Preserving Simplification of Real-World Firewall Rule Sets (abstract)
11:00
Automated Verification of RPC Stub Code (abstract)
11:30
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (abstract)
12:00
A Fully Verified Container Library (abstract)
10:30-12:30 Session 6B: IDay Papers
Chair:
Location: Smalltalk
10:30
Using Simulink Design Verifier for Automatic Generation of Requirements-based Tests (abstract)
10:50
Practices for Formal Models as Documents: Evolution of VDM Application to ``Mobile FeliCa" IC Chip Firmware (abstract)
11:10
Formalizing the Concept Phase of Product Development at Philips Healthcare (abstract)
11:30
Analyzing the Restart Behavior of Industrial Control Applications (abstract)
11:50
Software Development and Authentication for Arms Control Information Barriers (abstract)
14:00-15:30 Session 7A: Memory Models
Location: Simula
14:00
Verifying Opacity of a Transactional Mutex Lock (abstract)
14:30
A framework for correctness criteria on weak memory models (abstract)
15:00
Property-Driven Fence Insertion using Reorder Bounded Model Checking (abstract)
14:00-15:30 Session 7B: IDay Papers
Location: Smalltalk
14:00
Autofunk: an inference-based formal model generation framework for production systems. (abstract)
14:20
Eliminating Static Analysis False Positives using Loop Abstraction and Bounded Model Checking (abstract)
14:40
Formal Virtual Modelling and Data Verification for Supervision Systems (abstract)
15:00
Case Study: Static Security Analysis of the Android Goldfish Kernel (abstract)
Friday, June 26th

View this program: with abstractssession overviewtalk overview

09:00-10:00 Session 9: Keynote
Location: Simula
09:00
The key role of formal methods to overcome the interoperability challenge. (abstract)
10:30-12:30 Session 10: Model Checking
Chair:
Location: Simula
10:30
Certificates for Parameterized Model Checking (abstract)
11:00
Proving Safety with Trace Automata and Bounded Model Checking (abstract)
11:30
QPMC: A Model Checker for Quantum Programs and Protocols (abstract)
11:45
Automated Circular Assume-Guarantee Reasoning (abstract)
12:15
Model-Based Problem Solving for University Timetable Validation and Improvement (abstract)
14:00-15:30 Session 11: Static Analysis
Location: Simula
14:00
Narrowing operators on template abstract domains (abstract)
14:30
Static Differential Program Analysis for Software-Defined Networks (abstract)
15:00
Static Optimal Scheduling for Synchronous Data Flow Graphs with Model Checking (abstract)
16:00-17:30 Session 12: Logics and Semantics
Location: Simula
16:00
The Semantics of Cardinality-based Feature Models via Formal Languages (abstract)
16:30
Towards Formal Verification of Orchestration Computations Using the K Framework (abstract)
17:00
Typed First-Order Logic (abstract)