Abstract is missing.
- Programs as Paths: An Approach to Timing Constraint AnalysisIan J. Hayes. 1-15 [doi]
- Model Based Code VerificationColin O Halloran. 16-25 [doi]
- Adding Formalism to Methods or ::::Where and When Will Industry Use Formal Reasoning?::::Mathai Joseph. 26-33 [doi]
- Using Formal Methods to Serialize Synchronization EventsJessica Chen. 34-47 [doi]
- An AMBA-ARM7 Formal Verification PlatformKong Woei Susanto, Thomas F. Melham. 48-67 [doi]
- Formalization, Testing and Execution of a Use Case DiagramWuwei Shen, Shaoying Liu. 68-85 [doi]
- Service-Based Systems Engineering: Consistent Combination of ServicesBernhard Schätz, Chris Salzmann. 86-104 [doi]
- Using State Diagrams to Describe Concurrent BehaviourJim Davies, Charles Crichton. 105-124 [doi]
- The Equivalence of StatechartsQuan Long, Zongyan Qiu, Shengchao Qin. 125-143 [doi]
- Generic Interacting State Machines and Their Instantiation with Dynamic FeaturesDavid von Oheimb, Volkmar Lotz. 144-166 [doi]
- Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow LanguageSanjai Rayadurgam, Anjali Joshi, Mats Per Erik Heimdahl. 167-186 [doi]
- Formalising an Integrated Language in PVSGwen Salaün, Christian Attiogbé. 187-205 [doi]
- Modeling System C Fixed-Point Arithmetic in HOLBehzad Akbarpour, Sofiène Tahar. 206-225 [doi]
- Adding Action Refinement to Stochastic True Concurrency ModelsMila E. Majster-Cederbaum, Jinzhao Wu. 226-245 [doi]
- Incremental Derivation of Abstraction Relations for Data RefinementNeil J. Robinson. 246-265 [doi]
- Comparison of Data and Process RefinementSteve Reeves, David Streader. 266-285 [doi]
- Compilation by Refinement for a Practical Assembly LanguageGeoffrey Watson. 286-305 [doi]
- Java Card Code Generation from B SpecificationsBruno Tatibouët, Antoine Requet, Jean-Christophe Voisinet, Ahmed Hammad. 306-318 [doi]
- Efficient Path Finding with the Sweep-Line Method Using External StorageLars Michael Kristensen, Thomas Mailund. 319-337 [doi]
- Formal Development of a Distributed Logging Mechanism Supporting Disconnected UpdatesYuechen Qian. 338-358 [doi]
- Formal Proof of a Polychronous Protocol for Loosely Time-Triggered ArchitecturesMickaël Kerboeuf, David Nowak, Jean-Pierre Talpin. 359-374 [doi]
- A Z Based Approach to Verifying Security ProtocolsBenjamin W. Long, Colin J. Fidge, Antonio Cerone. 375-395 [doi]
- A Refinement Tool for ZAngela Freitas, Carla Nascimento, Ana Cavalcanti. 396-415 [doi]
- The Common Semantic Constructs of XML FamilyHong Li Yang, Jun Gang Han, Ke Gang Hao. 416-431 [doi]
- Controller Synthesis for Object Petri NetsBerndt Farwer, Saraswati Kalvala, Kundan Misra. 432-451 [doi]
- Towards a Workflow Model of Real-Time Cooperative SystemsYuyue Du, Changjun Jiang. 452-470 [doi]
- New Developments in Closed-Form Computation for GSPN AggregationJörn Freiheit, Jonathan Billington. 471-490 [doi]
- On Clock Difference Constraints and Termination in Reachability Analysis of Timed AutomataJohan Bengtsson, Wang Yi. 491-503 [doi]
- Analyzing the Redesign of a Distributed Lift System in UPPAALJun Pang, Bart Karstens, Wan Fokkink. 504-522 [doi]
- Verification of Timeliness QoS Properties in Multimedia SystemsBehzad Bordbar, Kozo Okano. 523-540 [doi]
- A Calculus for Set-Based Program DevelopmentGeorg Struth. 541-559 [doi]
- Compositional Verification of a Switch Fabric from Nortel NetworksHong Peng, Sofiène Tahar, Yassine Mokhtari. 560-578 [doi]
- Constraint-Based Model Checking of Data-Independent SystemsBeata Sarna-Starosta, C. R. Ramakrishnan. 579-598 [doi]
- A Formal Model for the Block Device Subsystem of the Linux KernelPeter T. Breuer. 599-619 [doi]
- A Mathematical Framework for SafechartsHamdan Dammag, Nimal Nissanke. 620-640 [doi]
- A Relational Model for Formal Object-Oriented Requirement Analysis in UMLZhiming Liu, Jifeng He, Xiaoshan Li, Yifeng Chen. 641-664 [doi]
- From Specification to Hardware Device: A Synthesis AlgorithmVincenza Carchiolo, Michele Malgeri, Giuseppe Mangioni. 665-681 [doi]