I've been struggling with understanding of the proofs showing that implementation statements are extensional. Basically I am referring to material described in Abstraction Classes in Software Design ...
I've been struggling with understanding of the proofs showing that tactical design statements are intensional and local. Basically I am referring to this material: Abstraction Classes in Software ...
Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?
(note: this is probably a beginner question, and English is not my first language) Recently, I have read a paper that used the “Java Modeling Language” (JML), see for instance: ...
What is the best way to describe the semantics of a new access control model?. I heard the temporal logic is the way to go. Is it true?
The Halting problem states that it is impossible to write a program that can determine if another program halts, for all possible input programs. I can, however, certainly write a program that can ...
I am self learning formal methods. I heard that formal methods is used (and usually only used) to create mission critical software (such as nuclear reactor controller, aircraft flight controller, ...
Does anyone know if the verified software repository is still alive? Bar that, are there other repositories out there of verified (or just certified) software? The archive of formal proofs is nice, ...
In the process of creating an AST analysis framework one of the challenges is creating good reusable functions and to avoid too much boiler-plate code. To that end catamorphisms seem like a good fit, ...