-
1
-
Validity Checking of Putback Transformations in Bidirectional Programming
-
16
-
Proof Engineering Considered Essential
-
22
-
Engineering <Emphasis FontCategory="SansSerif">UToPiA</Emphasis>
-
42
-
40 Years of Formal Methods
-
62
-
A Refinement Based Strategy for Local Deadlock Analysis of Networks of CSP Processes
-
78
-
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools
-
94
-
Definition, Semantics, and Analysis of Multirate Synchronous AADL
-
110
-
<Emphasis Type="SmallCaps">TrustFound</Emphasis>: Towards a Formal Foundation for Model Checking Trusted Computing Platforms
-
127
-
The VerCors Tool for Verification of Concurrent Programs
-
132
-
Knowledge-Based Automated Repair of Authentication Protocols
-
148
-
A Simplified Z Semantics for Presentation Interaction Models
-
163
-
Log Analysis for Data Protection Accountability
-
179
-
Automatic Compositional Synthesis of Distributed Systems
-
194
-
Automated Real Proving in PVS via MetiTarski
-
200
-
Quiescent Consistency: Defining and Verifying Relaxed Linearizability
-
215
-
Temporal Precedence Checking for Switched Models and Its Application to a Parallel Landing Protocol
-
230
-
Contracts in Practice
-
247
-
When Equivalence and Bisimulation Join Forces in Probabilistic Automata
-
263
-
Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs
-
279
-
Proof Patterns for Formal Methods
-
296
-
Efficient Runtime Monitoring with Metric Temporal Logic: A Case Study in the Android Operating System
-
312
-
<Emphasis Type="SmallCaps">iscas</Emphasis>M<Emphasis Type="SmallCaps">c</Emphasis>: A Web-Based Probabilistic Model Checker
-
318
-
Invariants, Well-Founded Statements and Real-Time Program Algebra
-
335
-
Checking Liveness Properties of Presburger Counter Systems Using Reachability Analysis
-
351
-
A Symbolic Algorithm for the Analysis of Robust Timed Automata
-
367
-
Revisiting Compatibility of Input-Output Modal Transition Systems
-
382
-
Co-induction Simply
-
399
-
Management of Time Requirements in Component-Based Systems
-
416
-
Compositional Synthesis of Concurrent Systems through Causal Model Checking and Learning
-
432
-
Formal Verification of Operational Transformation
-
449
-
Verification of a Transactional Memory Manager under Hardware Failures and Restarts
-
465
-
SCJ: Memory-Safety Checking without Annotations
-
481
-
Refactoring, Refinement, and Reasoning
-
497
-
Object Propositions
-
514
-
Flexible Invariants through Semantic Collaboration
-
531
-
Efficient Tight Field Bounds Computation Based on Shape Predicates
-
547
-
A Graph-Based Transformation Reduction to Reach UPPAAL States Faster
-
563
-
Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison
-
579
-
Efficient Self-composition for Weakest Precondition Calculi
-
595
-
Towards a Formal Analysis of Information Leakage for Signature Attacks in Preferential Elections
-
611
-
Analyzing Clinical Practice Guidelines Using a Decidable Metric Interval-Based Temporal Logic
-
627
-
A Modular Theory of Object Orientation in Higher-Order UTP
-
643
-
Formalizing and Verifying a Modern Build Language
-
658
-
The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification
-
673
-
Formally Verifying Graphics FPU
-
688
-
MDP-Based Reliability Analysis of an Ambient Assisted Living System
-
703
-
Diagnosing Industrial Business Processes: Early Experiences
-
718
-
Formal Verification of Lunar Rover Control Software Using UPPAAL
-
733
-
Formal Verification of a Descent Guidance Control Program of a Lunar Lander
