### Skapa referens, olika format (klipp och klistra)

**Harvard**

Kovacs, L. (2016) *Symbolic Computation and Automated Reasoning for Program Analysis*. Cham : Springer Verlag

** BibTeX **

@conference{

Kovacs2016,

author={Kovacs, Laura},

title={Symbolic Computation and Automated Reasoning for Program Analysis},

booktitle={Integrated Formal Methods},

isbn={978-3-319-33693-0},

pages={20-27},

abstract={This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the logically complex parts of software. The talk will first present how computer algebra methods, such as Grobner basis computation, quantifier elimination and algebraic recurrence solving, help us in inferring properties of program loops with non-trivial arithmetic. Typical properties inferred by our work are loop invariants and expressions bounding the number of loop iterations. The talk will then describe our work to generate first-order properties of programs with unbounded data structures, such as arrays. For doing so, we use saturation-based first-order theorem proving and extend first-order provers with support for program analysis. Since program analysis requires reasoning in the combination of first-order theories of data structures, the talk also discusses new features in first-order theorem proving, such as inductive reasoning and built-in boolean sort. These extensions allow us to express program properties directly in first-order logic and hence use further first-order theorem provers to reason about program properties.},

publisher={Springer Verlag},

place={Cham},

year={2016},

keywords={p-solvable loops, prover },

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 240642

A1 Kovacs, Laura

T1 Symbolic Computation and Automated Reasoning for Program Analysis

YR 2016

T2 Integrated Formal Methods

SN 978-3-319-33693-0

SP 20

OP 27

AB This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the logically complex parts of software. The talk will first present how computer algebra methods, such as Grobner basis computation, quantifier elimination and algebraic recurrence solving, help us in inferring properties of program loops with non-trivial arithmetic. Typical properties inferred by our work are loop invariants and expressions bounding the number of loop iterations. The talk will then describe our work to generate first-order properties of programs with unbounded data structures, such as arrays. For doing so, we use saturation-based first-order theorem proving and extend first-order provers with support for program analysis. Since program analysis requires reasoning in the combination of first-order theories of data structures, the talk also discusses new features in first-order theorem proving, such as inductive reasoning and built-in boolean sort. These extensions allow us to express program properties directly in first-order logic and hence use further first-order theorem provers to reason about program properties.

PB Springer Verlag

LA eng

DO 10.1007/978-3-319-33693-0_2

LK http://dx.doi.org/10.1007/978-3-319-33693-0_2

OL 30