🦞🌯 Lobster Roll

**Intro** I think there's enough formal methods fans posting and discussing this here that it'd be nice to have a specific tag for it. Some of the things it would cover: * Specification Techniques: TLA+, Alloy, Z notation * Model Checking: bisimulation, state machines * Verifiable Languages:...

I keep seeing books such as Software Foundations show up on forums with people interested in formal verification told they should look at them. I've watched people try and fail to learn this stuff for years. Very few make it. Some even get bitter against the concept of formal methods because they at...

DARPA's HACMS Program aims to create high-assurance, secure software for vehicles. This comprehensive article on HACMS introduces risks of computers, some techniques for assuring them, some cutting-edge results high assurance, phases of HACMS itself, impediments to using formal methods, and open cha...

Abstract: "Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running on a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challengi...

(I changed title to equivalent one that fits in blank.) Abstract: "Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most time and effort that is invested in proving is act...

Abstract: "In this thesis, I propose a methodology for supporting the development of software that depends on parsers—such as anything connected to the Internet—to safely support any reasonably designed protocol: data structures to describe protocol messages; validation routines that check that data...

DOI: [https://doi.org/10.1016/j.jlamp.2016.08.006](https://doi.org/10.1016/j.jlamp.2016.08.006)

Abstract: "We survey the use of Abstract State Machines in the area of programming languages, namely to define behavioral properties of programs at source, intermediate and machine levels in a way that is amenable to mathematical and experimental analysis by practitioners, like correctness and compl...

Abstract: "Bad smells are usually related to program source code, arising from bad design and programming practices. Refactoring activities are often motivated by the detection of bad smells. With the increasing adoption of Design-by-Contract (DBC) methodologies in formal software development, evide...

Abstract: "It is possible to make Integrated Development Environments supporting formal methods that can be as flexible as the support for dynamic programming languages. This paper contributes with a demonstration employing different support environments for the Vienna Development Method Specificati...

Abstract: "Despite extensive evangelizing and demonstration of several success stories in safety-critical applications, formal methods are still not widely practiced in contemporary systems and software engineering. One of the main reasons for this situation is the absence of systematic guidelin...

Abstract: "Graphics processing units (GPUs) are highly parallel processors that are now commonly used in the acceleration of a wide range of computationally intensive tasks. GPU programs often suffer from data races and deadlocks, necessitating systematic testing. Conventional GPU debuggers are i...

(This paper is from the First Workshop on Formal Methods in Software Engineering Education and Training in 2015) From the abstract (yes, I'm abstracting the abstract, because it actually is too long!): "[Formal Methods] plays just a minor role in both the everyday work of software engineers as...

I've ploped down some cash to gauge interest in a formal methods meetup. If you're interested in learning and leveraging more formal artefacts in day to day software engineering then please go ahead and sign up while I figure out the logistics. My current plan is to make it a mix of reading books...