🦞🌯 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...

Abstract: "A self-adaptive software system modifies its behavior at runtime in response to changes within the system or in its execution environment. The fulfillment of the system requirements needs to be guaranteed even in the presence of adverse conditions and adaptations. Thus, a key challenge fo...

(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...