Marco Bernardo, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Ina Schaefer
Advanced Lectures of the 14th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Formal Methods for Executable Software Models
SFM, 2014.

@proceedings{SFM-2014,
	address       = "Bertinoro, Italy",
	doi           = "10.1007/978-3-319-07317-0",
	editor        = "Marco Bernardo and Ferruccio Damiani and Reiner Hähnle and Einar Broch Johnsen and Ina Schaefer",
	isbn          = "978-3-319-07316-3",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Advanced Lectures of the 14th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Formal Methods for Executable Software Models}",
	volume        = 8483,
	year          = 2014,
}

Event page: http://www.sti.uniurb.it/events/sfm14esm/

Contents (8 items)

3 ×#concurrent
3 ×#modelling
2 ×#execution
2 ×#generative
2 ×#testing

SFM-2014-BubelMH #analysis #execution #modelling

Analysis of Executable Software Models (RB, AFM, RH), pp. 1–25.

SFM-2014-GiachinoL #concurrent #detection #linear #recursion #source code

Deadlock Detection in Linear Recursive Programs (EG, CL), pp. 26–64.

SFM-2014-AbrahamBDJKW #generative #markov #modelling #overview

Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey (EÁ, BB, CD, NJ, JPK, RW), pp. 65–121.

SFM-2014-GmeinerKSVW #algorithm #distributed #fault tolerance #model checking #tutorial

Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms (AG, IK, US, HV, JW), pp. 122–171.

SFM-2014-AmighiBDHMZ #concurrent #verification

Verification of Concurrent Systems with VerCors (AA, SB, SD, MH, WM, MZS), pp. 172–216.

SFM-2014-BoerG #monitoring #runtime

Combining Monitoring with Run-Time Assertion Checking (FSdB, SdG), pp. 217–262.

SFM-2014-AlbertAGR #concept #concurrent #execution #generative #symbolic computation #testing

Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency (EA, PA, MGZ, JMR), pp. 263–309.

SFM-2014-LochauPKS #modelling #testing

Model-Based Testing (ML, SP, MK, IS), pp. 310–342.