<oai_dc:dc xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:oai_dc="http://www.openarchives.org/OAI/2.0/oai_dc/" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://www.openarchives.org/OAI/2.0/oai_dc/ http://www.openarchives.org/OAI/2.0/oai_dc.xsd">
  <dc:contributor>Sharygina, Natasha</dc:contributor>
  <dc:creator>Tsitovich, Aliaksei</dc:creator>
  <dc:date>2011-02-23</dc:date>
  <dc:description xmlns:ns0="xml" ns0:lang="en">Following the industrial demand to address the problem of software correctness, the computer science research community puts a lot of efforts into development of scalable and precise formal methods  that are applicable to industrial-size programs. Unfortunately, most of software verification techniques suffer from the effect of combinatorial blowup also known as a "state-space explosion", i.e., situation,  when the size of the system state space and, consequently, the complexity of the verification problem grows exponentially in the size of the input program. This thesis tackles this problem by development  of new abstraction techniques as well as novel approaches of employing already existing ones. The results were used to construct algorithms for software verification and static analysis that discover  security faults in low-level C programs. First, this thesis presents a new algorithm that combines precise (but slow)} abstraction method with over-approximated (but fast) one in the abstraction-refinement  loop. It starts with the coarse over-approximated abstraction and then refines precisely, but restricts the refinement only to a subset of system state space that is related to a spurious counter-example  discovered in the previous verification step of the abstraction-refinement loop. Thus, it is possible to keep the refinement computational burden low and decrease the number of required refinement iterations  at the same time. We also propose a threshold-based optimization that further controls precise computation in order to avoid the unnecessary application of expensive quantifier elimination. Second, this  work defines a new technique for program abstraction. Unlike traditional program approximation approaches (e.g., abstract interpretation) it does not employ iterative fixpoint computation, instead it uses a  new summarization algorithm that non-iteratively computes symbolic abstract transformers with respect to a set of abstract domains. Summaries are shorter, loop-free program fragments, which are used  to substitute the original loops to obtain a conservative abstraction of the program. Our approach computes abstract transformers starting from the inner-most loop. It obtains a loop invariant by checking if  the constraints defined by a chosen abstract domain are preserved by the loop. These checks are performed by means of calls to a quantifier-free decision procedure, which allows us to check (possibly  infinite) sets of states with one query. Thus, unlike other approaches, our algorithm is not restricted to finite-height domains.Therefore, it allows for effective usage of problem-specific abstract domains for  summarization and, as a consequence, precision of an abstract model can be tuned for specific verification needs. In particular, several memory operations-related abstract domains were applied to  perform static analysis of programs for buffer overflows. Third, this thesis addresses the problem of scalable program termination analysis. Termination of a (sequential) program can be concluded from  termination of all its loops. Existing algorithms rely on iterative enumeration of all paths through a program (loop) and construction of a valid termination argument (well-founded transition invariant) for each of  them using available ranking discovery methods. Instead, we present a new algorithm that applies relational abstract domains for loop summarization to discover transition invariants. Well-foundedness can  be ensured either by separate decision procedure call (though it requires quantifier elimination) or by using the abstract domains that are well-founded by construction.Such a light-weight approach to  termination analysis was demonstrated to be effective on a wide range of benchmarks, including the OS device drivers.</dc:description>
  <dc:format>application/pdf</dc:format>
  <dc:identifier>https://n2t.net/ark:/12658/srd1318314</dc:identifier>
  <dc:identifier>https://susi.usi.ch/global/documents/318314</dc:identifier>
  <dc:identifier>https://susi.usi.ch/documents/318314/files/2011INFO008.pdf</dc:identifier>
  <dc:language>eng</dc:language>
  <dc:relation>info:eu-repo/semantics/altIdentifier/urn/urn:nbn:ch:rero-006-110231</dc:relation>
  <dc:relation>info:eu-repo/semantics/altIdentifier/ark/12658/srd1318314</dc:relation>
  <dc:rights>info:eu-repo/semantics/openAccess</dc:rights>
  <dc:rights>License undefined</dc:rights>
  <dc:subject xmlns:ns1="xml" ns1:lang="en">Abstraction</dc:subject>
  <dc:subject xmlns:ns2="xml" ns2:lang="en">Abstraction-refinement loop</dc:subject>
  <dc:subject xmlns:ns3="xml" ns3:lang="en">Over-approximation</dc:subject>
  <dc:subject xmlns:ns4="xml" ns4:lang="en">Invariants</dc:subject>
  <dc:subject xmlns:ns5="xml" ns5:lang="en">Loop invariants</dc:subject>
  <dc:subject xmlns:ns6="xml" ns6:lang="en">Transition invariants</dc:subject>
  <dc:subject xmlns:ns7="xml" ns7:lang="en">Termination</dc:subject>
  <dc:subject xmlns:ns8="xml" ns8:lang="en">Infinite loops</dc:subject>
  <dc:subject xmlns:ns9="xml" ns9:lang="en">Static analysis</dc:subject>
  <dc:subject xmlns:ns10="xml" ns10:lang="en">Symbolic execution</dc:subject>
  <dc:subject>info:eu-repo/classification/udc/004</dc:subject>
  <dc:title xmlns:ns11="xml" ns11:lang="en">Scalable abstractions for efficient security checks</dc:title>
  <dc:type>http://purl.org/coar/resource_type/c_db06</dc:type>
</oai_dc:dc>