23

In general you cannot determine complexity, even for halting programs: let $T$ be some arbitrary Turing machine and let $p_T$ be the program (that always returns 0): input: n run T for n steps if T is in halting state, output: 0 otherwise, loop for n^2 steps and output: 0 It is clear that it is undecidable in general whether $p_T$ is linear-time or ...


11

The question you pose and the specific counting trick you describe is a classic one in program analysis. There is the theoretical problem of complexity analysis, and it's practical manifestation in terms of automatically estimating the performance of a piece of code. Such an automated analysis has several applications from detecting performance bugs to ...


11

The question is rather broad. To answer it in a reasonable space I will make many oversimplifications. Let us agree on terminology. A program is correct when it implies its specification. This vague statement is made precise in many ways, by pinning down what exactly is a program and what exactly is a specification. For example, in model checking the ...


8

One approach to reducing the gap between a program and its specification is to use a language with a formal semantics. An interesting example here would be Esterel. Have a look at Gérard Berry's web page for some interesting talks about his work bringing formal methods into the real world. http://www-sop.inria.fr/members/Gerard.Berry/ p.s. Been on an ...


7

The science of building reliable software in the "real world" is still being developed and is to some degree verging on an inherently cultural or anthropological study, because computers and software dont "cause" bugs— humans do! this answer will focus on general Q/A approaches of which formal software verification can be seen as one element. a remarkable ...


6

An old approach (but it is still used in some applications) is the N-version programming From Wikipedia: N-version programming (NVP), also known as multiversion programming, is a method or process in software engineering where multiple functionally equivalent programs are independently generated from the same initial specifications. The concept of N-...


5

Don't worry too much about understanding everything in one source. Try reading several different articles and from their summaries and technical details, you may build up your own understanding. Symbolic Execution for Software Testing: Three Decades Later, Cristian Cadar and Koushik Sen, 2013. All You Ever Wanted to Know about Dynamic Taint Analysis and ...


3

Two or three years ago I started taking a look to formal methods applied to software. This was a quest driven by curiosity, and by the feeling that I had to learn programming tools and methods with longer time-spans. Although I dreamed wishfully about a Silver Bullet, I really thought that there was not an answer to the question: "How can I write a correct ...


3

This is a strange comparison. Your question is comparable to asking "how expressive is the ANSI C language specification compared to stdlib and compilation". The comparisons don't make sense. The Java Modelling Language can be used as a specification language to specify properties of code. The language alone does not solve the problem of verifying whether ...


3

This kind of "laws" are usually labelled as Pareto principle, or 80–20 rule: Answering specifically your question(s) 1) This law is true in the real sense, or is just an observation, a presumption? This law is just an observation, and was explained more formally as a property of exponential distributions or power law. Then the observation is just the ...


1

Being a beginner to Symbolic Execution (SE) myself, I would suggest: Symbolic execution and program testing: this is the paper to cite when you mention SE. It is easy to read, and provides the key idea without much logical formulation. All you ever wanted to know...: this paper surveys SE and its applications to Security. The third step may be to ...


1

There were a lot of publication on extending and or formalizing RBAC/SOD with LTL or other flavors of temporal logics, not sure of other AC models. Google Scholar (or simple google) search with yield a bunch of articles. Most of them might be not sufficiently formal for somebody like yourself, yet might be of some interest. Not sure is LTL the best way. Yet ...


1

The answers so far covered already most of what should be said about the foundations of how relate specification and code to each other. I just want to add a more practical point that approaches the question in the header of this thread: How create mission critical software? There exists tools that automatically analyze your code for errors (violations ...


Only top voted, non community-wiki answers of a minimum length are eligible