The tag has no wiki summary.

learn more… | top users | synonyms

-1
votes
1answer
381 views

Program optimization - 90/10 law

I found this "law" somewhere on Wikipedia: In software engineering, it is often a better approximation that 90% of the execution time of a computer program is spent executing 10% of the code ...
0
votes
2answers
222 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
0answers
104 views

Proofs for Implementation Statements

I've been struggling with understanding of the proofs showing that implementation statements are extensional. Basically I am referring to material described in Abstraction Classes in Software Design ...
0
votes
1answer
199 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: ...
0
votes
0answers
89 views

Temporal Logic and Access Control Models

What is the best way to describe the semantics of a new access control model?. I heard the temporal logic is the way to go. Is it true?
18
votes
2answers
550 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
736 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, ...
6
votes
0answers
126 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, ...
2
votes
0answers
100 views

Recursion Schemes for Static Analysis (AST)

In the process of creating an AST analysis framework one of the challenges is creating good reusable functions and to avoid too much boiler-plate code. To that end catamorphisms seem like a good fit, ...