The formal-methods tag has no wiki summary.
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 ...
13
votes
7answers
503 views
Pointers for CS applications of logic
I'm a grad student in math with a solid background in logic. I've taken a year-long graduate course in logic together with graduate courses on finite model theory and another on forcing and set ...
2
votes
1answer
90 views
How to auto-derivate sequential iterative programs from a mathematical specification?
I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory.
First, write down the formal specification as a Hoare triple and figure ...
3
votes
3answers
193 views
Is it possible to compute whether two functions are extensional equal?
If you have two functions implementing a different sorting algorithm, is it then possible to infer by source code that they both have the same external properties? Meaning that they both will have a ...
2
votes
1answer
84 views
Formal Methods Applied to Role-Based Security (RBAC)
I wonder if someone could direct me to a basic introduction to formal methods applied to role-based security. I'm particularly interested in the question of formal verification and the kind of ...
14
votes
2answers
375 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
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, ...
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 ...
4
votes
1answer
207 views
What are the limitations on formal proofs of Erlang systems?
Well, today I just got my 15 minutes of fame, but now I think I am wrong on the point about formal proofs on Erlang systems. The discussion on news.ycombinator.com suggests that Erlang code may or ...
0
votes
0answers
189 views
Viola Jones algorithm information/descriprion [closed]
I need the information about using the Viola Jones algorithm in video object tracking/detection. Rather the frame processing stages while object tracking/detection.
P.S. sorry for my English and sorry ...
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.
...
0
votes
0answers
174 views
formal definition of “flowcharts”
I am looking for a formal definition of so-called "flowcharts" used as representation of programs or business processes.
Is there some good one around ?
Thx
JCLL
16
votes
7answers
853 views
How can we know that formal methods work?
An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be ...
21
votes
6answers
570 views
Curriculum: Logical/Formal Methods in Security
At present I teach a small course (Four two hour lectures at the Masters level) on Logical Methods in Security, though the title Formal Methods in Security might be more apt. It covers briefly the ...
