Given a specification, does a program satisfy it?
0
votes
1answer
101 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:
...
5
votes
1answer
89 views
Step-indexing: Where to begin?
I am about to begin a verification project (for MIPS) with my professor (I am a senior undergraduate) and have been told that the soundness proof for the program logic we need will probably involve ...
3
votes
3answers
152 views
Can Hoare logic be used when objects are created or deleted?
Hoare logic can be used for proving program correctness (e.g. for deriving correctness statements for the whole program from the statements for the individual commands or constructions; good summary ...
9
votes
2answers
226 views
Original Hoare Logic termination paper
I'm looking for the original paper where Hoare (or someone else I suppose) discusses termination (Total Correctness). Or any other early work on termination for "vanilla" Hoare logic (I suppose by ...
10
votes
8answers
574 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, ...
7
votes
1answer
227 views
Proofs techniques related to Curry–Howard correspondence
I am looking for sources about formalized notion of programs. This seems to be closely related to Curry-Howard correspondence, but one could also track this back to Universal Turing Machines and its ...
8
votes
2answers
241 views
Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)
I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, ...
5
votes
1answer
370 views
How to use induction without Fixpoint definition in Coq?
I want to verify a program written in C. I am using Jessie to translate the (pre/post)conditions of the program to Coq. In Coq I will make a proof. Sometimes I need recursive definitions.
...
9
votes
0answers
244 views
What is the proper role of verification in quantum sampling, simulation, and extended-Church-Turing (E-C-T) testing?
Since no answer was given, a flag has been set requesting that this question be converted to a community wiki.
The comments by Aaron Sterling, Sasho Nikolov, and Vor have been synthesized into the ...
6
votes
2answers
236 views
What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?
I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation.
For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want ...
20
votes
4answers
564 views
Relationship between contracts and dependent typing
I've been reading some articles on dependent types and programming contracts. From the majority of what I've read, it seems that contracts are dynamically checked constraints and dependent types are ...
12
votes
6answers
457 views
What are practically computable properties of Labelled Transition Systems?
I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would ...
2
votes
1answer
663 views
What's the difference between an invariant and an “inductive” invariant?
I would like to understand this with an example. Also, are there other kinds of invariants related to these?
Thanks!
14
votes
3answers
376 views
How hard is it to reduce termination to partial correctness?
If you are familiar with program verification you are likely to prefer reading the Question before the Background. If you are not familiar with program verification then you may still be able to ...
