Modular, crash-safe refinement for ASMs with submachines

Börger, 2003 Börger, 2003, The ASM refinement method, Form. Asp. Comput., 15, 237, 10.1007/s00165-003-0012-7 Joshi, 2007, A mini challenge: build a verifiable filesystem, Form. Asp. Comput., 19, 269, 10.1007/s00165-006-0022-3 Reeves, 2005, The Mars Rover Spirit FLASH anomaly, 4186 Schellhorn, 2014, Development of a verified flash file system, vol. 8477, 9 Ernst Ernst, 2015, KIV – overview and verify this competition, Softw. Tools Technol. Transf., 17, 677, 10.1007/s10009-014-0308-3 Woodcock, 1996 Ernst, 2014, Modular refinement for submachines of ASMs, vol. 8477, 188 Ernst, 2012, A formal model of a virtual filesystem switch, 33 Ernst, 2014, Verification of a virtual filesystem switch, vol. 8164, 242 Harel, 2000 Reif, 1998, Structured specifications and interactive proofs with KIV, 13 Pfähler, 2013, Formal specification of an erase block management layer for flash memory, vol. 8244, 214 Ernst, 2016, Inside a verified flash file system: transactions & garbage collection, vol. 9593, 73 He, 1986, Data refinement refined, 187 Schellhorn, 2005, ASM refinement and generalizations of forward simulation in data refinement: a comparison, J. Theor. Comput. Sci., 336, 403, 10.1016/j.tcs.2004.11.013 de Roever, 1998, Data Refinement: Model-Oriented Proof Methods and Their Comparison, vol. 47 Schellhorn, 2001, Verification of ASM refinements using generalized forward simulation, J. Univers. Comput. Sci., 7, 952 Schellhorn, 2009, Completeness of fair ASM refinement, Sci. Comput. Program., 76, 756, 10.1016/j.scico.2009.10.004 Abrial, 2010 Abrial, 1996 Börger, 2000, Composition and submachine concepts for sequential ASMs, vol. 1862, 41 Abrial, 2007, Refinement, decomposition, and instantiation of discrete models: application to Event-B, Fundam. Inform., 77, 1 Damchoom, 2009, Applying event and machine decomposition to a flash-based filestore in Event-B, 134 Hoare, 1985 McEwan, 2010, Unifying theories of interrupts, vol. 5713, 122 Roscoe, 1997 Sivathanu, 2005, A logic of file systems, vol. 5, 1 Bornholt, 2016, Specifying and checking file system crash-consistency models, 83 Klein, 2009, seL4: formal verification of an OS kernel, 207 Baumann, 2009, Verifying the PikeOS Microkernel: an overview of the verisoft XT Avionics Project Kang, 2009, Designing and analyzing a flash file system with alloy, Int. J. Softw. Inform., 3, 129 Jackson, 2006 Taverne, 2009, RAFFS: model checking a robust abstract flash file store, 226 Yang, 2004, Using model checking to find serious file system errors, 273 Ridge, 2015, SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems Marić, 2014, Verification of a transactional memory manager under hardware failures and restarts, vol. 8442, 449 Chen, 2015, Specifying crash safety for storage systems Chen, 2015, Using crash hoare logic for certifying the FSCQ file system, 18 Ntzik, 2015, Fault-tolerant resource reasoning, vol. 9458, 169 Koskinen, 2016, Reducing crash recoverability to reachability Keller, 2013, File systems deserve verification too!, 1 O'Connor-Davis, 2014 Amani, 2015, Specifying a realistic file system, 1 Lali, 2013, File system formalization: revisited, Int. J. Adv. Comput. Sci., 3, 602 Schellhorn, 2014, RGITL: a temporal logic framework for compositional reasoning about interleaved programs, Ann. Math. Artif. Intell., 71, 131, 10.1007/s10472-013-9389-z