Uncategorized http://verify.inf.unisi.ch/research/ Lists all the projects en Detection of Security Flaws and Vulnerabilities by Guided Model Checking http://verify.inf.unisi.ch/projects/DSFVGMC <p>Modern information-driven society has &nbsp;an obvious need for security measures that can safeguard the storage and transfer of sensitive information. Software is responsible for almost 100% of the data manipulation in the world and, thus, should be placed under particularly strict security control. Unfortunately, writing a program devoid of bugs is still one of the greatest challenges for developers. As a result, low level implementation mistakes lead not only to software malfunction, but also to security breaches.</p> <p><a href="http://verify.inf.unisi.ch/projects/DSFVGMC">read more</a></p> Sun, 02 Dec 2007 03:45:52 +0100 mcWebAdmin 6 at http://verify.inf.unisi.ch Automated Invariant Discovery for Array-based Systems http://verify.inf.unisi.ch/invariants <p>The research problem addressed by this project is the development of techniques and tools for automated discovering of loop invariants. Infinite program fragments such as loops or recursive functions should be represented by a finite summary, i.e., an invariant, in order to succeed in their verification. Moreover, retrieving an invariant it&rsquo;s mandatory if we want to model check function handling unbounded data structures (e.g., a function that sorts an input array of unknown length). Such invariants are represented as quantified formulae over the variables of the program.</p> <p><a href="http://verify.inf.unisi.ch/invariants">read more</a></p> Tue, 17 Jan 2012 15:22:45 +0100 Francesco 147 at http://verify.inf.unisi.ch Formal verification of software changes and upgrades http://verify.inf.unisi.ch/upgrades <p class="p1">The project addresses the problem of checking of software upgrades. Serving this goal, state-of-the-art model checkers hardly use the information of the old version, and reduce it thereby to the standalone verification.&nbsp;The purpose of the research is to develop a new technique for checking the software upgrades based on successful verification of the old program and reuse of the invested effort.&nbsp;</p> <p><a href="http://verify.inf.unisi.ch/upgrades">read more</a></p> Tue, 18 Oct 2011 10:49:08 +0200 mcWebAdmin 139 at http://verify.inf.unisi.ch The Synergy of Precise and Fast Abstractions for Program Veriļ¬cation http://verify.inf.unisi.ch/projects/synergy <p>Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to the predicates. Given a set of predicates, a precise abstraction contains the minimal set of transitions, but as a result is computationally expensive. Most model checkers therefore approximate the abstraction to alleviate the computation of the abstract system by trading off precision with cost. <p><a href="http://verify.inf.unisi.ch/projects/synergy">read more</a></p> Sun, 19 Oct 2008 04:11:45 +0200 mcWebAdmin 66 at http://verify.inf.unisi.ch Automated Verification of Security Policies in Mobile Code http://verify.inf.unisi.ch/projects/AVSPMC <p>This project defines a model checking-based approach for verification of mobile programs against security policies.</p> <p><a href="http://verify.inf.unisi.ch/projects/AVSPMC">read more</a></p> Tue, 16 Sep 2008 19:59:52 +0200 mcWebAdmin 63 at http://verify.inf.unisi.ch Formal Verification via Boolean and Theory Reasoning (SMT) http://verify.inf.unisi.ch/projects/SMT <p>State-of-the-art techniques used in <strong>Formal Verification</strong> ultimately rely on the expression of properties (of the system to verify) in terms of languages that can be easily understood and processed by automatic tools.</p> <p><a href="http://verify.inf.unisi.ch/projects/SMT">read more</a></p> Mon, 21 Jan 2008 10:43:31 +0100 Roberto 42 at http://verify.inf.unisi.ch