Runtime enforcement of timed properties using games Matthieu RenardAntoine RolletYliès Falcone Original Paper 28 July 2020 Pages: 315 - 360
Formal Verification of Robotic Cell Injection systems up to 4-DOF using HOL Light Adnan RashidOsman Hasan OriginalPaper 22 June 2020 Pages: 229 - 250
Theoretical and Practical Approaches to the Denotational Semantics for MDESL based on UTP Feng ShengHuibiao ZhuJonathan P. Bowen Original Article 15 June 2020 Pages: 275 - 314
Legislation-driven development of a Gift Aid system using Event-B David M. WilliamsSalaheddin DarwishDavid R. Michael Original Article Open access 25 May 2020 Pages: 251 - 273
Collaborative models for autonomous systems controller synthesis Douglas FraserRuben GiaquintaGethin Norman Original Article Open access 16 April 2020 Pages: 157 - 186
PuRSUE -from specification of robotic environments to synthesis of controllers Marcello M. BersaniMatteo SoldoMatteo Rossi Original Article Open access 23 March 2020 Pages: 187 - 227
Stepwise development and model checking of a distributed interlocking system using RAISE S. GeislerA. E. Haxthausen Original Article 21 February 2020 Pages: 87 - 125
Formal analysis of the compact position reporting algorithm Aaron DutleMariano MoscatoFrançois Bobot Original Article 11 February 2020 Pages: 65 - 86
Gerard O’Regan: Concise Guide to Formal Methods: Theory, Fundamentals and Industry Applications Jonathan P. Bowen Book Review 05 February 2020 Pages: 147 - 148
Using formal verification to evaluate the execution time of Spark applications L. BaresiM. M. BersaniM. Rossi Original Article 05 February 2020 Pages: 33 - 70
André Platzer: Logical foundations of cyber-physical systems Alexander KnappMarkus Roggenbach Book Review Open access 20 March 2020 Pages: 149 - 151
Modeling and Verification of A Timing Protection Mechanism in the OSEK/VDX OS using CSP Yanhong HuangHaiping PangJianqi Shi Original Article 25 May 2020 Pages: 113 - 145
Formal reliability and failure analysis of ethernet based communication networks in a smart grid substation Waqar AhmadOsman HasanSofiène Tahar Original Article 27 January 2020 Pages: 71 - 111
Correction to: Multiple model synchronization with multiary delta lenses with amendment and K-Putput Zinovy DiskinHarald KönigMark Lawford Correction 15 January 2020 Pages: 153 - 153
Fifty years of Hoare’s logic Krzysztof R. AptErnst-Rüdiger Olderog Original Article 27 November 2019 Pages: 751 - 807
Zohar Manna (1939–2018) Nachum DershowitzRichard Waldinger Obituary 27 November 2019 Pages: 643 - 660
Linearizability on hardware weak memory models Graeme SmithKirsten WinterRobert J. Colvin Original Article 15 November 2019 Pages: 1 - 32
Bisimulation and Coinduction Enhancements: A Historical Perspective Damien PousDavide Sangiorgi OriginalPaper 08 November 2019 Pages: 733 - 749
Bernhard Steffen, Oliver R¨uthing, and Michael Huth: Mathematical Foundations of Advanced Informatics—Volume 1: Inductive Approaches Greg Michaelson Book Review 22 October 2019 Pages: 641 - 642
Multiple model synchronization with multiary delta lenses with amendment and K-Putput Zinovy DiskinHarald KönigMark Lawford Original Article 22 October 2019 Pages: 611 - 640
Assembling a prehistory for formal methods: a personal view Thomas Haigh OriginalPaper 25 September 2019 Pages: 663 - 674
From LCF to Isabelle/HOL Lawrence C. PaulsonTobias NipkowMakarius Wenzel Original Article Open access 02 September 2019 Pages: 675 - 698
Estimating costs of multi-component enterprise applications Antonio BrogiAndrea CorradiniJacopo Soldani Original Article 21 August 2019 Pages: 421 - 451
Read atomic transactions with prevention of lost updates: ROLA and its formal analysis Si LiuPeter Csaba ÖlveczkyJosé Meseguer Original Article 02 August 2019 Pages: 503 - 540
Milestones from the Pure Lisp theorem prover to ACL2 J. Strother Moore Original Article 30 July 2019 Pages: 699 - 732
Interactive verification of architectural design patterns in FACTum Diego MarmsolerHabtom Kashay Gidey Original Article 30 July 2019 Pages: 541 - 610
Discovering and correcting a deadlock in a channel implementation Gavin Lowe Original Article Open access 15 July 2019 Pages: 411 - 419
Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds): Handbook of model checking Igor Konnov Book Review 21 June 2019 Pages: 455 - 456
A verification-driven framework for iterative design of controllers Claudio MenghiPaola SpoletiniCarlo Ghezzi Original Article Open access 05 June 2019 Pages: 459 - 502
John Fitzgerald, Peter Gorm Larsen, Marcel Verhoef (eds): Collaborative design for embedded systems Richard Banach Book Review 04 June 2019 Pages: 453 - 454
Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving Pedro AntoninoThomas Gibson-RobinsonA. W. Roscoe Original Article Open access 13 May 2019 Pages: 375 - 409
Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example Cliff B. JonesNisansala Yatapanage Original Article Open access 15 April 2019 Pages: 353 - 374
Finding suitable variability abstractions for lifted analysis Aleksandar S. DimovskiClaus BrabrandAndrzej Wąsowski Original Article 15 March 2019 Pages: 231 - 259
A modeling and verification framework for optical quantum circuits Sidi Mohamed BeillahiMohamed Yousri MahmoudSofiène Tahar Original Article 15 March 2019 Pages: 321 - 351
Consistency-preserving refactoring of refinement structures in Event-B models Tsutomu KobayashiFuyuki IshikawaShinichi Honiden Original Article 11 February 2019 Pages: 287 - 320
Automating Event-B invariant proofs by rippling and proof patching Yuhui LinAlan BundyEwen Maclean Original Article Open access 02 January 2019 Pages: 95 - 129
Formal reliability analysis of redundancy architectures Marco BozzanoAlessandro CimattiCristian Mattarei Original Article 02 January 2019 Pages: 59 - 94
Extensional Petri net Xiaoju DongYuxi FuDaniele Varacca Original Article 16 November 2018 Pages: 47 - 58
Special section of Tests and Proofs 2016 Bernhard K. AichernigCarlo A. FuriaRob Hierons Editorial 13 November 2018 Pages: 627 - 628
Egon Börger and Alexander Raschke: Modeling companion for software practitioners Jonathan P. Bowen Book Review 22 October 2018 Pages: 761 - 762
Automated mutual induction proof in separation logic Quang-Trung TaTon Chanh LeWei-Ngan Chin Original Article 11 October 2018 Pages: 207 - 230
Hybrid statistical estimation of mutual information and its application to information flow Fabrizio BiondiYusuke KawamotoLouis-Marie Traonouez Original Article 08 October 2018 Pages: 165 - 206
GPU-accelerated steady-state computation of large probabilistic Boolean networks Andrzej MizeraJun PangQixia Yuan Original Article 04 October 2018 Pages: 27 - 46
Formal analysis of the kinematic Jacobian in screw theory Zhiping ShiAixuan WuXiaoyu Song Original Article 24 September 2018 Pages: 739 - 757
