This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...
This thesis tackles new challenges associated with the disaggregate modeling of the human behavior. Decision-aid tools help in making decisions, by providing quantitative insights on the decisions and associated consequences. They are useful in complex sit ...
Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. TM shifts the burden of managing concurrency from the programmer to the TM algorithm. The correctness of TM algorithms is generally proved manually. The goal ...
The formal specification component of verification can be exported to simulation through the idea of property checkers. The essence of this approach is the automatic construction of an observer from the specification in the form of a program that can be in ...
In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexampl ...