Formal Aspects of Computing, Volume 23

Volume 23, Number 1, January 2011

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

Volume 23, Number 2, March 2011

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

Volume 23, Number 3, May 2011

• Axel van Lamsweerde:
  The Humble Humorous Researcher: A Tribute to Michel Sintzoff. 239-242
  
• Geoffrey M. Brown, Lee Pike:
  Automated verification and refinement for physical-layer protocols. 243-266
  
• Ioannis T. Kassios:
  The dynamic frames theory. 267-288
  
• Cliff B. Jones, Ken G. Pierce:
  Elucidating concurrent algorithms via layers of abstraction and reification. 289-306
  
• Daniel Sinnig, Ferhat Khendek, Patrice Chalin:
  Partial order semantics for use case and task models. 307-332
  
• Wil 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. 333-363
  
• Gerard J. Holzmann, Mihai Florian:
  Model checking with bounded context switching. 365-389
  

Volume 23, Number 4, July 2011

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

Volume 23, Number 5, September 2011

• Daniel Kroening, Tiziana Margaria, Jim Woodcock:
  Editorial. 585-588
  
• Sven Jörges, Tiziana Margaria, Bernhard Steffen:
  Assuring property conformance of code generators via model checking. 589-606
  
• Murali 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. 607-626
  
• Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi:
  A model checking-based approach for security policy verification of mobile systems. 627-648
  
• K. Mani Chandy, Brian Go, Sayan Mitra, Concetta Pilotto, Jerome White:
  Verification of distributed systems with local-global predicates. 649-679
  

Volume 23, Number 6, November 2011

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

Last update Sat May 25 20:11:14 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page