The se.software-engineering tag has no wiki summary.
1
vote
0answers
86 views
Proofs for Implementation Statements
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 ...
0
votes
0answers
88 views
Proofs for Design Statements
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 ...
0
votes
1answer
97 views
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:
...
0
votes
0answers
83 views
Temporal Logic and Access Control Models
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?
14
votes
2answers
369 views
To what extent can an algorithm predict the time complexity an arbitrary input program?
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 ...
10
votes
8answers
570 views
How to Create Mission Critical Software?
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, ...
5
votes
0answers
103 views
Verified Software Repository
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, ...
2
votes
0answers
90 views
Recursion Schemes for Static Analysis (AST)
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, ...
