Journal: Formal Asp. Comput.

Volume 17, Issue 4

389 -- 389Eerke Boiten, John Derrick, Graeme Smith. Guest Editorial Integrated Formal Methods
390 -- 422Steve Schneider, Helen Treharne. CSP theorems for communicating B machines
423 -- 442Bernhard Beckert, Steffen Schlager. Refinement and retrenchment for programming language data types
443 -- 460Jifeng He, Dang Van Hung, Geguang Pu, Zongyan Qiu, Wang Yi. Exploring optimal solution to hardware/software partitioning for synchronous model
461 -- 483Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha. Concurrent software verification with states, events, and deadlocks

Volume 17, Issue 3

259 -- 259John Cooke. Editorial
260 -- 276Sigrid Gürgens, Carsten Rudolph. Security analysis of efficient (Un-)fair non-repudiation protocols
277 -- 318Andrew D. Gordon, Riccardo Pucella. Validating a web service security abstraction by typing
319 -- 341Martin De Wulf, Laurent Doyen, Jean-François Raskin. Almost ASAP semantics: from timed models to timed implementations
342 -- 388Bahareh Badban, Wan Fokkink, Jan Friso Groote, Jun Pang, Jaco van de Pol. Verification of a sliding window protocol in µCRL and PVS

Volume 17, Issue 2

91 -- 92Michael Leuschel. Guest Editorial
93 -- 112A. W. Roscoe. On the expressive power of CSP refinement
113 -- 137Michael Huth. Refinement is complete for implementations
138 -- 159Stefano Cattani, Marta Z. Kwiatkowska. A refinement-based process algebra for timed automata
160 -- 176Gethin J. Norman, David Parker, Marta Z. Kwiatkowska, Sandeep K. Shukla, Rajesh Gupta. Using probabilistic model checking for dynamic power management
177 -- 200Bram De Wachter, Alexandre Genon, Thierry Massart, Cédric Meuter. The formal design of distributed controllers with ::d::SL and Spin
201 -- 221Elsa L. Gunter, Doron Peled. Model checking, testing and verification working together
222 -- 257Roberto Bagnara, Patricia M. Hill, Enea Zaffanella. Not necessarily closed convex polyhedra and the double description method

Volume 17, Issue 1

1 -- 18Dominikus Herzberg, Manfred Broy. Modeling layered distributed communication systems
19 -- 37Jan Friso Groote, François Monin, Jan Springintveld. A computer checked algebraic verification of a distributed summation algorithm
38 -- 57Andrew Cook, Andrew Ireland, Greg Michaelson, Norman Scaife. Discovering applications of higher order functions through proof planning
58 -- 68Sidi O. Ehmety, Lawrence C. Paulson. Mechanizing compositional reasoning for concurrent systems: some lessons
69 -- 90Ralph-Johan Back, Viorel Preoteasa. An algebraic treatment of procedure refinement to support mechanical verification