Journal: Formal Asp. Comput.

Volume 23, Issue 6

681 -- 0Ana Cavalcanti, Dennis Dams, Marie-Claude Gaudel. Editorial
683 -- 709Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge. Automated property verification for large scale B models with ProB
711 -- 737A. K. McIver, Carroll C. Morgan. Compositional refinement in agent-based security protocols
739 -- 779Mark Reynolds. A tableau-based decision procedure for CTL
781 -- 805Chao Wang, Sudipta Kundu, Rhishikesh Limaye, Malay K. Ganai, Aarti Gupta. Symbolic predictive analysis for concurrent programs

Volume 23, Issue 5

585 -- 588Daniel Kroening, Tiziana Margaria, Jim Woodcock. Editorial
589 -- 606Sven Jörges, Tiziana Margaria, Bernhard Steffen. Assuring property conformance of code generators via model checking
607 -- 626Murali Sitaraman, Bruce M. Adcock, Jeremy Avigad, Derek Bronish, Paolo Bucci, David Frazier, Harvey M. Friedman, Heather K. Harton, Wayne D. Heym, Jason Kirschenbaum, Joan Krone, Hampton Smith, Bruce W. Weide. Building a push-button RESOLVE verifier: Progress and challenges
627 -- 648Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi. A model checking-based approach for security policy verification of mobile systems
649 -- 679K. Mani Chandy, Brian Go, Sayan Mitra, Concetta Pilotto, Jerome White. Verification of distributed systems with local-global predicates

Volume 23, Issue 4

391 -- 419Eric C. R. Hehner. A probability perspective
421 -- 432Alan Stewart. A programming model for BSP with partitioned synchronisation
433 -- 463José Luiz Fiadeiro, Antónia Lopes, Laura Bocchi. An abstract model of service discovery and binding
465 -- 512Ana Cavalcanti, Phil Clayton, Colin O Halloran. From control law diagrams to Ada via ::::Circus::::
513 -- 539Linmin Yang, Zhe Dang, Thomas R. Fischer. Information gain of black-box testing
541 -- 565Han Gao, Flemming Nielson, Hanne Riis Nielson. CaPiTo: protocol stacks for services

Volume 23, Issue 3

239 -- 242Axel van Lamsweerde. The Humble Humorous Researcher: A Tribute to Michel Sintzoff
243 -- 266Geoffrey M. Brown, Lee Pike. Automated verification and refinement for physical-layer protocols
267 -- 288Ioannis T. Kassios. The dynamic frames theory
289 -- 306Cliff B. Jones, Ken G. Pierce. Elucidating concurrent algorithms via layers of abstraction and reification
307 -- 332Daniel Sinnig, Ferhat Khendek, Patrice Chalin. Partial order semantics for use case and task models
333 -- 363Wil M. P. van der Aalst, Kees M. van Hee, Arthur H. M. ter Hofstede, Natalia Sidorova, H. M. W. Verbeek, Marc Voorhoeve, Moe Thandar Wynn. Soundness of workflow nets: classification, decidability, and analysis
365 -- 389Gerard J. Holzmann, Mihai Florian. Model checking with bounded context switching

Volume 23, Issue 2

151 -- 0Zhiming Liu, Jim Woodcock. Editorial
153 -- 170Andrew Butterfield. A denotational semantics for Handel-C
171 -- 190Bican Xia, Lu Yang, Naijun Zhan, Zhihai Zhang. Symbolic decision procedure for termination of linear programs
191 -- 219Anne Elisabeth Haxthausen, Jan Peleska, Sebastian Kinder. A formal approach for the construction and verification of railway control systems
221 -- 238Peter D. Mosses. VDM semantics of programming languages: combinators and monads

Volume 23, Issue 1

1 -- 2Egon Börger. Editorial
3 -- 19Jacques Julliand, Pierre-Alain Masson, Régis Tissot, Pierre-Christophe Bué. Generating tests from B specifications and dynamic selection criteria
21 -- 41Alessandra Cavarra. A data-flow approach to test multi-agent ASMs
43 -- 71John Derrick, Siobhán North, Anthony J. H. Simons. Z2SAL: a translation-based model checker for Z
73 -- 89Stephen Wright, Kerstin Eder. Using Event-B to construct instruction set architectures
91 -- 112Simon Bäumler, Gerhard Schellhorn, Bogdan Tofan, Wolfgang Reif. Proving linearizability with temporal logic
113 -- 131Richard Banach. Retrenchment for Event-B: UseCase-wise development and Rodin integration
133 -- 150Stefan Hallerstede. On the purpose of Event-B proof obligations