The tag has no wiki summary.

learn more… | top users | synonyms

23
votes
5answers
923 views

Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
6
votes
1answer
270 views

Describing state machines mathematically

The short paper "Computer Science and State Machines" by Leslie Lamport seems quite strange to me. On the one hand, I am surprised to see that an important hardware protocol called "two-phase ...
4
votes
2answers
112 views

Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?

I've been going over some material related to IPC recently from Tanenbaum's "Modern Operating Systems" and revisited semaphore after many years. There is a lot of code and pseudo code based ...
0
votes
2answers
228 views

Help in understanding Symbolic Execution

I am an undergraduate CS student and currently reading on software security, particularly on static analysis of programs. I am particularly interested in understanding Symbolic Execution - an ...
0
votes
1answer
207 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: ...
6
votes
1answer
117 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
665 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
106 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 ...
6
votes
3answers
291 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
98 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 ...
18
votes
2answers
553 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 ...
13
votes
9answers
741 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
252 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
242 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 ...
6
votes
1answer
520 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
198 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
19
votes
7answers
952 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
616 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 ...