Questions tagged [formal-methods]

Formal methods are stringent mathematical techniques to model systems to verify their properties to guarantee reliability.

Filter by
Sorted by
Tagged with
1 vote
0 answers
133 views

Operational semantics and denotational semantics and describing the behaviour and structure of programs

I was under the impression that operational semantics describes the behaviour of a program (so it includes the implementation details / the implementation matters), whereas denotational semantics ...
The Pointer's user avatar
2 votes
2 answers
77 views

State machine classes with sub-exponentially growing model spaces

State machines are useful tools for system modelling. They allow for a compact visual notation of discrete systems and provide a formal model of them. However, reasoning about the correctness of an ...
stateMachineOperator's user avatar
1 vote
0 answers
52 views

Is this proof for completeness of regular model checking correct?

In "Calculational Design of A Regular Model Checker by Abstract Interpretation" by Patrick Cousot (link), on page 15 it can be seen that to prove the completeness of regular model checking (...
Senmorta's user avatar
4 votes
3 answers
128 views

Formalization of matching logic (logic behind K Framework)

Is there any mechanization for matching logic (any flavor)? I only find study about K Framework rules to Deducti translation, but this is both not covering to matching logic and not internalizing the ...
uhbif19's user avatar
  • 305
3 votes
1 answer
50 views

Equivalence of finitary and infinitary semantics of concurrent programs

The following claim is stated on p. 155 of Manna and Pnueli's The Temporal Logic of Reactive and Concurrent Systems: Specification. Let $P_1$ and $P_2$ be two finitely branching transition systems ...
Evan Aad's user avatar
  • 354
0 votes
1 answer
100 views

What is "structural model checking"?

In "Calculational Desing of a Regular Model Checker by Abstract Interpretation" (see) Cousot first defines a definition of model checking in his new settings at the page 9 then at the page ...
Senmorta's user avatar
0 votes
1 answer
69 views

Proper terminology for input, parameter or variable fixing. Refinement? Projection? Fixation? Partial valuation?

I contemplate writing a paper on automating fixing some inputs/parameters to specific values in a kind of workflow/pipeline definition language/system and looking for best terminology. English is not ...
Serge's user avatar
  • 111
1 vote
1 answer
73 views

What is region construction in timed automata?

I've recently started self-learning timed automata. There's this theorem in there that a timed automaton can be converted to a DFA using a "region" construction. I've looked up references on ...
whoisit's user avatar
  • 125
2 votes
0 answers
86 views

From formal models to programs - Model Checking

I am reading on Automata, Model Checking and CTL/LTL. I am looking for examples/references/books that help me understand the following: Given a program (for example Python or Java), how can I change ...
Karl 17302's user avatar
6 votes
0 answers
231 views

Satisfiability and a Galois Theory Analog

Let $v(a, b)$ be a binary predicate, and define $\phi$ as follows: $$\phi: v(a_1, b_1) \land v(a_1, b_2) \land (a_1, b_3)$$ where our universe consists of two sorts $A: \{a_1, a_2, a_3\}$ and $B: \{...
Steven Schaefer's user avatar
4 votes
1 answer
137 views

A possible error in the semantic chapter of the ISO standard for the Z specification notation

I may have found an error in the ISO standards document for the Z specification notation, namely ISO/IEC 13568:2002, "Information technology — Z formal specification notation — Syntax, type ...
Evan Aad's user avatar
  • 354
3 votes
1 answer
207 views

Looking for an online community specializing in the Z specification language, where I can ask questions

Where can I find an online community specializing in the Z specification language, where I can ask specific questions about the ISO standard for Z?
Evan Aad's user avatar
  • 354
2 votes
1 answer
402 views

Defining finite sets inductively in a proof assistant?

To represent finite sets within coq, we either use something like ListSet, which are just definitions on top of list, or we ...
Siddharth Bhat's user avatar
1 vote
1 answer
115 views

Running an algorithm for fixed amount of time on RAM model machine

Suppose there is a deterministic algorithm of size $O(1)$ that operates on an input of size $N$ on a RAM model machine. I want to run the algorithm for $O(\sqrt{N})$ time, pause the algorithm, print "...
karmanaut's user avatar
  • 1,177
4 votes
0 answers
141 views

A reasonable proof strategy for formally verifying Ukkonen's algorithm?

What's a reasonable proof strategy to formally verify Ukkonen's algorithm in, say, Coq? The ingredients as far as I can tell would be: some form of separation logic to be able to reason about the ...
Siddharth Bhat's user avatar
1 vote
0 answers
83 views

Journals or conferences to submit formally verified libraries?

This is a soft question aimed at understanding whether there is any value to publishing formally verified libraries. I have formally verified (in Coq) implementations of: synthetic differential ...
Siddharth Bhat's user avatar
6 votes
1 answer
158 views

SMT solving with less-than theory and monotonic functions

I am attempting to solve a less-than theory within an SMT paradigm that involves variables assigned to reals and assumes that all the functions used in the theory are monotonic. The theory's signature ...
C. Bowers's user avatar
1 vote
1 answer
2k views

Difference between CTMC, DTMC, and MDP

I've been reading the Handbook of Model Checking recently; I'm especially interested in probabilistic model checking, so have been led to the PRISM model checker. For background, I am very familiar ...
ahelwer's user avatar
  • 151
1 vote
1 answer
197 views

How are safety/liveness languages defined on the set of finite or infinite words?

Let $Σ$ be an alphabet (e.g., the powerset of atomic propositions coming from some Kripke structure, though such details are irrelevant here). For infinite words, a language $P\subseteq Σ^ω$ is ...
user avatar
1 vote
0 answers
54 views

How to justify this causally consistent execution in the $(vis, ar)$ framework for distributed consistency models?

In Figure 5.1 of the book "Principles of Eventual Consistency" by Sebastin Burckhardt, 2014, Causal Consistency (CC); wiki is (mainly) defined as the conjunction of $hb \subseteq vis$ and $hb \...
hengxin's user avatar
  • 2,329
1 vote
0 answers
110 views

Confusion about the visibility and arbitration relations in a formal framework for distributed consistency models

In the POPL'14 paper "Replicated Data Types: Specification, Verification, Optimality" and the book "Principles of Eventual Consistency", the authors propose a formal framework for ...
hengxin's user avatar
  • 2,329
5 votes
1 answer
234 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 ...
hengxin's user avatar
  • 2,329
2 votes
1 answer
59 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 ...
user1868607's user avatar
7 votes
1 answer
125 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 (SCT). Let $G$ satisfy the SCT condition. There is an effective procedure to construct a $...
user1868607's user avatar
14 votes
1 answer
501 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-...
user1868607's user avatar
6 votes
1 answer
331 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 ...
lightning's user avatar
  • 433
-1 votes
1 answer
59 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 ...
Sebastian Bechtel's user avatar
1 vote
0 answers
193 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 ...
Nathan BeDell's user avatar
7 votes
1 answer
145 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 ...
hengxin's user avatar
  • 2,329
2 votes
2 answers
158 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 ...
Lance's user avatar
  • 141
2 votes
0 answers
74 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 ...
SorcererofDM's user avatar
0 votes
0 answers
180 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 ...
qartal's user avatar
  • 101
0 votes
0 answers
67 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 ...
qartal's user avatar
  • 101
-2 votes
1 answer
164 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 ...
MainstreamDeveloper00's user avatar
1 vote
0 answers
57 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 ...
liyu's user avatar
  • 11
25 votes
5 answers
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 ...
Nathan BeDell's user avatar
6 votes
1 answer
456 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 ...
hengxin's user avatar
  • 2,329
5 votes
2 answers
198 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 ...
vin's user avatar
  • 161
2 votes
2 answers
800 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 ...
dmkathayat's user avatar
1 vote
1 answer
618 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....
mrsteve's user avatar
  • 443
8 votes
1 answer
599 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 ...
C.E.Sally's user avatar
  • 313
18 votes
7 answers
1k 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
1 answer
129 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 ...
Chuck's user avatar
  • 23
9 votes
3 answers
1k 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 ...
Matthijs Steen's user avatar
2 votes
1 answer
130 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 ...
user10756's user avatar
23 votes
2 answers
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 ...
Hooked's user avatar
  • 365
15 votes
9 answers
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, ...
fajrian's user avatar
  • 251
8 votes
1 answer
387 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 ...
AllCoder's user avatar
  • 191
5 votes
1 answer
557 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 ...
ConcernedOfTunbridgeWells's user avatar
7 votes
1 answer
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. ...
Anton's user avatar
  • 71