-
1
-
Looking Back to the Future
-
7
-
Past, Present, and Future of SRA Implementation of <Emphasis FontCategory="SansSerif">CafeOBJ</Emphasis>
-
18
-
On Failures and Faults
-
40
-
Trends in Software Verification
-
51
-
Event Based Sequential Program Development: Application to Constructing a Pointer Program
-
75
-
Proving the Shalls
-
94
-
Adaptable Translator of <Emphasis FontCategory="SansSerif">B</Emphasis> Specifications to Embedded <Emphasis FontCategory="SansSerif">C</Emphasis> Programs
-
114
-
Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle
-
133
-
Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project
-
154
-
Determining the Specification of a Control System from That of Its Environment
-
170
-
Managerial Issues for the Consideration and Use of Formal Methods
-
187
-
Verifying Emulation of Legacy Mission Computer Systems
-
208
-
Improving Safety Assessment of Complex Systems: An Industrial Case Study
-
223
-
Compositional Verification of an ATM Protocol
-
244
-
Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method
-
264
-
Synthesis and Verification of Constraints in the PGM Protocol
-
282
-
Mapping Statecharts to Verilog for Hardware/Software Co-specification
-
301
-
A Strategy for Compiling Classes, Inheritance, and Dynamic Binding
-
321
-
A Semantic Foundation for TCOZ in Unifying Theories of Programming
-
341
-
Refinement and Verification of Synchronized Component-Based Systems
-
359
-
Certifying and Synthesizing Membership Equational Proofs
-
381
-
Team Automata Satisfying Compositionality
-
401
-
Composing Invariants
-
422
-
Java Applet Correctness: A Developer-Oriented Approach
-
440
-
Improving JML: For a Safer and More Effective Language
-
462
-
Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems
-
482
-
A Formal Framework for Modular Synchronous System Design
-
503
-
Generating Counterexamples for Multi-valued Model-Checking
-
522
-
Combining Real-Time Model-Checking and Fault Tree Analysis
-
542
-
Model-Checking TRIO Specifications in SPIN
-
562
-
Computing Meta-transitions for Linear Transition Systems with Polynomials
-
582
-
Translation-Based Compositional Reasoning for Software Systems
-
600
-
Watchdog Transformations for Property-Oriented Model-Checking
-
617
-
A <Emphasis FontCategory="SansSerif">C</Emphasis>ircus Semantics for Ravenscar Protected Objects
-
636
-
Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach
-
658
-
A General Approach to Deadlock Freedom Verification for Software Architectures
-
678
-
Taking <Emphasis Type="Italic">Alloy</Emphasis> to the Movies
-
698
-
Interacting State Machines for Mobility
-
719
-
Composing Temporal-Logic Specifications with Machine Assistance
-
739
-
Model Checking FTA
-
758
-
Program Checking with Certificates: Separating Correctness-Critical Code
-
778
-
Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study
-
796
-
Checking and Reasoning about Semantic Web through Alloy
-
814
-
Structuring Retrenchments in B by Decomposition
-
834
-
Design of an Automatic Prover Dedicated to the Refinement of Database Applications
-
855
-
ProB: A Model Checker for B
-
875
-
SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis
-
894
-
Correctness of Source-Level Safety Policies
-
914
-
A Topological Characterization of TCP/IP Security
-
-
-
Combining Real-Time Model-Checking and Fault Tree Analysis
