Abstract is missing.
- Program Verification Through Computer AlgebraZhou Chaochen. 1 [doi]
- JML s Rich, Inherited Specifications for Behavioral SubtypesGary T. Leavens. 2-34 [doi]
- Three Perspectives in Formal EngineeringJohn A. McDermid, Andy Galloway. 35-54 [doi]
- A Method for Formalizing, Analyzing, and Verifying Secure User InterfacesBernhard Beckert, Gerd Beuster. 55-73 [doi]
- Applying Timed Interval Calculus to Simulink DiagramsChunqing Chen, Jin Song Dong. 74-93 [doi]
- Reducing Model Checking of the Few to the OneE. Allen Emerson, Richard J. Trefler, Thomas Wahl. 94-113 [doi]
- Induction-Guided FalsificationKazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi. 114-131 [doi]
- Verifying ::::chi:::: Models of Industrial Systems with SpinNikola Trcka. 132-148 [doi]
- Stateful Dynamic Partial-Order ReductionXiaodong Yi, Ji Wang, Xuejun Yang. 149-167 [doi]
- User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service CompositionXiaoning Ding, Jun Wei, Tao Huang. 168-184 [doi]
- Environment Ontology-Based Capability Specification for Web Service DiscoveryPuwei Wang, Zhi Jin, Lin Liu. 185-205 [doi]
- Scenario-Based Component Behavior DerivationYan Zhang, Jun Hu, Xiaofeng Yu, Tian Zhang, Xuandong Li, Guoliang Zheng. 206-225 [doi]
- Verification of Computation Orchestration Via Timed AutomataJin Song Dong, Yang Liu, Jun Sun 0001, Xian Zhang. 226-245 [doi]
- Towards the Semantics for Web Service Choreography Description LanguageJing Li, Jifeng He, Geguang Pu, Huibiao Zhu. 246-263 [doi]
- Type Checking Choreography Description LanguageHongli Yang, Xiangpeng Zhao, Zongyan Qiu, Chao Cai, Geguang Pu. 264-283 [doi]
- Formalising Progress Properties of Non-blocking ProgramsBrijesh Dongol. 284-303 [doi]
- Towards a Fully Generic Theory of DataDouglas A. Creager, Andrew C. Simpson. 304-323 [doi]
- Verifying Statemate Statecharts Using CSP and FDRA. W. Roscoe, Zhenzhong Wu. 324-341 [doi]
- A Reasoning Method for Timed CSP Based on Constraint SolvingJin Song Dong, Ping Hao, Jun Sun 0001, Xian Zhang. 342-359 [doi]
- Mapping RT-LOTOS Specifications into Time Petri NetsTarek Sadani, Marc Boyer, Pierre de Saqui-Sannes, Jean-Pierre Courtiat. 360-379 [doi]
- Reasoning Algebraically About Probabilistic LoopsLarissa Meinicke, Ian J. Hayes. 380-399 [doi]
- Formal Verification of the Heap Manager of an Operating System Using Separation LogicNicolas Marti, Reynald Affeldt, Akinori Yonezawa. 400-419 [doi]
- A Statically Verifiable Programming Model for Concurrent Object-Oriented ProgramsBart Jacobs 0002, Jan Smans, Frank Piessens, Wolfram Schulte. 420-439 [doi]
- Model Checking Dynamic UML ConsistencyXiangpeng Zhao, Quan Long, Zongyan Qiu. 440-459 [doi]
- Conditions for Avoiding Controllability Problems in Distributed TestingJessica Chen, Lihua Duan. 460-477 [doi]
- Generating Test Cases for Constraint Automata by Genetic Symbiosis AlgorithmSamira Tasharofi, Sepand Ansari, Marjan Sirjani. 478-493 [doi]
- Checking the Conformance of Java Classes Against Algebraic SpecificationsIsabel Nunes, Antónia Lopes, Vasco Thudichum Vasconcelos, João Abreu, Luís S. Reis. 494-513 [doi]
- Incremental SlicingHeike Wehrheim. 514-528 [doi]
- Assume-Guarantee Software Verification Based on Game SemanticsAleksandar Dimovski, Ranko Lazic. 529-548 [doi]
- Optimized Execution of Deterministic Blocks in Java PathFinderMarcelo d Amorim, Ahmed Sobeih, Darko Marinov. 549-567 [doi]
- A Tool for a Formal Pattern Modeling LanguageSoon-Kyeong Kim, David A. Carrington. 568-587 [doi]
- An Open Extensible Tool Environment for Event-BJean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Laurent Voisin. 588-605 [doi]
- Tool for Translating Simulink Models into Input Language of a Model CheckerB. Meenakshi, Abhishek Bhatnagar, Sudeepa Roy. 606-620 [doi]
- Verifying Abstract Information Flow Properties in Fault Tolerant Security DevicesTim McComb, Luke Wildman. 621-638 [doi]
- A Language for Modeling Network AvailabilityLuigia Petre, Kaisa Sere, Marina A. Waldén. 639-659 [doi]
- Multi-process Systems Analysis Using Event B: Application to Group Communication SystemsChristian Attiogbé. 660-677 [doi]
- Issues in Implementing a Model Checker for ZJohn Derrick, Siobhán North, Tony Simons. 678-696 [doi]
- Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model CheckingLeo Freitas, Ana Cavalcanti, Jim Woodcock. 697-716 [doi]
- Discovering Likely Method SpecificationsNikolai Tillmann, Feng Chen, Wolfram Schulte. 717-736 [doi]
- Time Aware Modelling and Analysis of Multiclocked VLSI SystemsTomi Westerlund, Juha Plosila. 737-756 [doi]
- SALT - Structured Assertion Language for Temporal LogicAndreas Bauer 0002, Martin Leucker, Jonathan Streit. 757-775 [doi]