Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

The tag has no usage guidance.

5
votes
1answer
149 views

Confusion about a formal definition of PRAM consistency

I am reading the paper "Consistency in Non-Transactional Distributed Storage Systems" by Paolo Viotti and Marko Vukolić. The authors provide a comprehensive survey of various consistency semantics ...
2
votes
1answer
47 views

Ordering sequences containing bitvectors for size-change termination

I'm working with the size-change termination principle to show program termination. In the system I work with, there is a so-called bit-vector ordering that goes as follows: Given two sequences of ...
5
votes
1answer
74 views

Lee's algorithm for synthesis of ranking functions in size-change termination proofs

Consider the following statement that appeared in Lee's Ranking functions for size-change termination. Let $G$ satisfy the SCT condition. There is an effective procedure to construct a $G$-...
13
votes
0answers
246 views

Algebraic topology for termination proofs

I'm reading about various ways in which termination proofs of software verifiers are built: ad-hoc methods that detect recursions, term-rewriting, synthesis of lexicographic orderings... From the ad-...
6
votes
1answer
132 views

Ways to think formally about Satisfiability Modulo Theories

Apologies if this is not a well-thought-out question, but I am interested in formalizing a problem which is ultimately described by a SMT formula in the theory of quantified arrays and linear ...
-1
votes
1answer
47 views

semantics of “destroy object” in HRU model

In the access control model HRU there is the primitive request destroy object o which is only defined if o is an object in the current protection state which is not a subject. I am interested in why ...
1
vote
0answers
95 views

Have there been any practical applications of domain theory to formal methods?

By Domain Theory, I mean the use of CPOs (or related topological/order-theoretic structures) to study the denotational semantics of programming languages. Compared to the two other common approaches ...
7
votes
1answer
123 views

Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

In Section 4.3.2 entitled "Proof Method" of Herlihy and Wing, "Linearizability: A Correctness Condition for Concurrent Objects", 1990 the authors describe the technique for verifying ...
2
votes
2answers
126 views

Practical example: how to formally verify “file name” implementation from a spec?

Say you have an OS-independent specification for file names. The file names are case sensitive, and let's say can't be more than 200 characters, and can't have : or ...
2
votes
0answers
58 views

applications of institution-independent model theory

To quote wikipedia, The notion of institution has been created by Joseph Goguen and Rod Burstall in the late 1970s in order to deal with the "population explosion among the logical systems used in ...
0
votes
0answers
161 views

Theoretical background of Classes and Objects

I would like to learn about the possible ways of formalizing Classes and Objects (in programing languages like java) using formal languages. Where should I start? This might be related to my previous ...
0
votes
0answers
55 views

Specification language for specifying both Objects and Primitive data types

I am looking for an specification language, which supports both primitive data types and objects. I already know about Object-Z. But I am wondering if there is any other Specification language that I ...
-2
votes
1answer
134 views

What are the most fundamental metrics (criterions) of database performance?

I'm a student working on my thesis in database theory and looking for some research in the field of formal models of database performance and couldn't find any works in this area. I'm interested: what ...
1
vote
0answers
53 views

what is the meaning of “indicate substitution by priming metavariables”

This is a question about the usage of "indicate substitution by priming metavariables". For example, in the separation logic(it is not important whether familiar to this logic), I can understand the ...
24
votes
5answers
2k 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
368 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 ...
5
votes
2answers
178 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 ...
1
vote
2answers
557 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 ...
1
vote
1answer
398 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: http://www.eecs.ucf....
6
votes
1answer
159 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 ...
17
votes
7answers
908 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 theory....
2
votes
1answer
117 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 ...
9
votes
3answers
602 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
114 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 ...
22
votes
2answers
1k 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 ...
15
votes
9answers
2k 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, ...
8
votes
1answer
311 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 ...
5
votes
1answer
457 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 ...
7
votes
1answer
1k 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
205 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
20
votes
7answers
1k 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 ...
22
votes
6answers
703 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 ...