Università della Svizzera italiana

Reusing constraint proofs in symbolic analysis

Chen, Meixian ; Pezzè, Mauro (Dir.)

Thèse de doctorat : Università della Svizzera italiana, 2018 ; 2018INFO007.

Symbolic analysis is an important element of program verification and automatic testing. Symbolic analysis techniques abstract program properties as expressions of symbolic input values to characterise the program logical constraints, and rely on Satisfiability Modulo Theories (SMT) solvers to both validate the satisfiability of the constraint expression and verify the corresponding program...

Università della Svizzera italiana

Test generation for high coverage with abstraction refinement and coarsening (ARC)

Baluda, Mauro ; Pezzè, Mauro (Dir.) ; Denaro, Giovanni (Codir.)

Thèse de doctorat : Università della Svizzera italiana, 2014 ; 2014INFO018.

Testing is the main approach used in the software industry to expose failures. Producing thorough test suites is an expensive and error prone task that can greatly benefit from automation. Two challenging problems in test automation are generating test input and evaluating the adequacy of test suites: the first amounts to producing a set of test cases that accurately represent the software...

Università della Svizzera italiana

Scalable abstractions for efficient security checks

Tsitovich, Aliaksei ; Sharygina, Natasha (Dir.)

Thèse de doctorat : Università della Svizzera italiana, 2011 ; 2011INFO008.

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.,...