Journal: Formal Asp. Comput.

Volume 31, Issue 6

643 -- 660Nachum Dershowitz, Richard Waldinger. Zohar Manna (1939-2018)
661 -- 0Cliff Jones, José Oliveira. Editorial
663 -- 674Thomas Haigh. Assembling a prehistory for formal methods: a personal view
675 -- 698Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel. From LCF to Isabelle/HOL
699 -- 732J. Strother Moore. Milestones from the Pure Lisp theorem prover to ACL2
733 -- 749Damien Pous, Davide Sangiorgi. Bisimulation and Coinduction Enhancements: A Historical Perspective
751 -- 807Krzysztof R. Apt, Ernst-Rüdiger Olderog. Fifty years of Hoare's logic

Volume 31, Issue 5

457 -- 458Alessandra Russo, Andy Schürr, Heike Wehrheim. Editorial
459 -- 502Claudio Menghi, Paola Spoletini, Marsha Chechik, Carlo Ghezzi. A verification-driven framework for iterative design of controllers
503 -- 540Si Liu 0003, Peter Csaba Ölveczky, Qi Wang, Indranil Gupta, José Meseguer. Read atomic transactions with prevention of lost updates: ROLA and its formal analysis
541 -- 610Diego Marmsoler, Habtom Kahsay Gidey. Interactive verification of architectural design patterns in FACTum
611 -- 640Zinovy Diskin, Harald König, Mark Lawford. Multiple model synchronization with multiary delta lenses with amendment and K-Putput
641 -- 642Greg Michaelson. Bernhard Steffen, Oliver R¨uthing, and Michael Huth: Mathematical Foundations of Advanced Informatics - Volume 1: Inductive Approaches - Springer, 2 April 2018, 258 pp, 156x16x234mm, ISBN-13: 978-3319683966 (Hardback, £28.99), ISBN: 978-3030098339 (Paperback, £27.99)

Volume 31, Issue 4

411 -- 419Gavin Lowe. Discovering and correcting a deadlock in a channel implementation
421 -- 451Antonio Brogi, Andrea Corradini, Jacopo Soldani. Estimating costs of multi-component enterprise applications
453 -- 454Richard Banach. John Fitzgerald, Peter Gorm Larsen, Marcel Verhoef (eds): Collaborative design for embedded systems - Springer, Berlin Heidelberg, 2014
455 -- 456Igor Konnov 0001. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds): Handbook of model checking - Springer International Publishing AG, Cham, Switzerland, 2018

Volume 31, Issue 3

287 -- 320Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden. Consistency-preserving refactoring of refinement structures in Event-B models
321 -- 351Sidi Mohamed Beillahi, Mohamed Yousri Mahmoud, Sofiène Tahar. A modeling and verification framework for optical quantum circuits
353 -- 374Cliff B. Jones, Nisansala Yatapanage. Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
375 -- 409Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe. Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving

Volume 31, Issue 2

131 -- 132Stefania Gnesi, Ana Cavalcanti, John S. Fitzgerald, Constance L. Heitmeyer. Editorial
133 -- 163Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, Robert J. Colvin. A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
165 -- 206Fabrizio Biondi, Yusuke Kawamoto 0001, Axel Legay, Louis-Marie Traonouez. Hybrid statistical estimation of mutual information and its application to information flow
207 -- 230Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, Wei-Ngan Chin. Automated mutual induction proof in separation logic
231 -- 259Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski. Finding suitable variability abstractions for lifted analysis
261 -- 285Morten Bisgaard, David Gerhardt, Holger Hermanns, Jan Krcál, Gilles Nies, Marvin Stenger. Battery-aware scheduling in low orbit: the GomX-3 case

Volume 31, Issue 1

1 -- 0Martin Fränzle, Deepak Kapur, Heike Wehrheim, Naijun Zhan. Editorial
3 -- 25Mingsheng Ying. Toward automatic verification of quantum programs
27 -- 46Andrzej Mizera, Jun Pang, Qixia Yuan. GPU-accelerated steady-state computation of large probabilistic Boolean networks
47 -- 58Xiaoju Dong, Yuxi Fu, Daniele Varacca. Extensional Petri net
59 -- 94Marco Bozzano, Alessandro Cimatti, Cristian Mattarei. Formal reliability analysis of redundancy architectures
95 -- 129Yuhui Lin, Alan Bundy, Gudmund Grov, Ewen Maclean. Automating Event-B invariant proofs by rippling and proof patching