Person: Alberto Pettorossi

DBLP: Pettorossi:Alberto

Facilitated 1 volumes:

Ed

Contributed to:

2015

2015

2014

2014

2013

2014

2012

2011

2010

2010

2009

2008

2007

2006

2005

2004

2004

2002

2001

2000

2000

2000

1999

1999

1997

1996

1995

1994

1993

1992

1991

1991

1991

1990

1984

1981

1987

Wrote 38 papers:

ICLP-J-2015-AngelisFPP #correctness #horn clause #imperative #proving #source code

Proving correctness of imperative programs by linearizing constrained Horn clauses (EDA, FF, AP, MP), pp. 635–650.

PPDP-2015-AngelisFPP #generative #semantics #verification

Semantics-based generation of verification conditions by program specialization (EDA, FF, AP, MP), pp. 91–102.

TACAS-2014-AngelisFPP #named #source code #verification

VeriMAP: A Tool for Verifying Programs through Transformations (EDA, FF, AP, MP), pp. 568–574.

VMCAI-2014-AngelisFPP #array #source code #verification

Verifying Array Programs by Transforming Verification Conditions (EDA, FF, AP, MP), pp. 182–202.

PEPM-2013-AngelisFPP #source code #verification

Verifying programs via iterated specialization (EDA, FF, AP, MP), pp. 43–52.

PEPM-J-2013-AngelisFPP14 #verification

Program verification via iterated specialization (EDA, FF, AP, MP), pp. 149–175.

LOPSTR-2012-AngelisFPP #model checking

Specialization with Constrained Generalization for Software Model Checking (EDA, FF, AP, MP), pp. 51–70.

LOPSTR-2011-FioravantiPPS #using

Using Real Relaxations during Program Specialization (FF, AP, MP, VS), pp. 106–122.

ICLP-J-2010-PettorossiSP #infinity #logic programming #source code

Transformations of logic programs on infinite lists (AP, VS, MP), pp. 383–399.

LOPSTR-2010-FioravantiPPS #evaluation #infinity #verification

Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation (FF, AP, MP, VS), pp. 164–183.

LOPSTR-2009-PettorossiPS #branch #logic #program transformation

Deciding Full Branching Time Logic by Program Transformation (AP, MP, VS), pp. 5–21.

ICLP-2008-SenniPP #algorithm #constraints #logic programming #source code

A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs (VS, AP, MP), pp. 284–300.

ICLP-2007-PettorossiPS #automation #correctness #logic programming #program transformation #proving

Automatic Correctness Proofs for Logic Program Transformations (AP, MP, VS), pp. 364–379.

ICLP-2006-PettorossiPS #constraints #logic programming #proving #source code

Proving Properties of Constraint Logic Programs by Eliminating Existential Variables (AP, MP, VS), pp. 179–195.

LOPSTR-2005-PettorossiPS #array #protocol #using #verification

Transformational Verification of Parameterized Protocols Using Array Formulas (AP, MP, VS), pp. 23–43.

PDCL-2004-FioravantiPP #constraints #logic programming #source code

Transformation Rules for Locally Stratified Constraint Logic Programs (FF, AP, MP), pp. 291–339.

PEPM-2004-PettorossiP #formal method #logic programming #program transformation

A theory of totally correct logic program transformations (AP, MP), pp. 159–168.

LOPSTR-2002-FioravantiPP #higher-order #logic #logic programming #monad #program transformation #source code

Combining Logic Programs and Monadic Second Order Logics by Program Transformation (FF, AP, MP), pp. 160–181.

LOPSTR-2001-FioravantiPP #infinity #process #program transformation #set #using #verification

Verification of Sets of Infinite State Processes Using Program Transformation (FF, AP, MP), pp. 111–128.

CL-2000-PettorossiP #model checking

Perfect Model Checking via Unfold/Fold Transformations (AP, MP), pp. 613–628.

LOPSTR-2000-FioravantiPP #automation #constraints #logic programming #source code

Automated strategies for specializing constraint logic programs (FF, AP, MP).

LOPSTR-J-2000-FioravantiPP #automation #constraints #logic programming #source code

Automated Strategies for Specializing Constraint Logic Programs (FF, AP, MP), pp. 125–146.

ICLP-1999-ProiettiP #induction

Transforming Inductive Definitions (MP, AP), pp. 486–499.

LOPSTR-1999-PettorossiP #logic programming #source code

Transformation Rules for Logic Programs with Goals as Arguments (AP, MP), pp. 176–195.

POPL-1997-PettorossiPR #logic programming #nondeterminism #source code

Reducing Nondeterminism while Specializing Logic Programs (AP, MP, SR), pp. 414–427.

LOPSTR-1996-PettorossiPR #deduction

Enhancing Partial Deduction via Unfold/Fold Rules (AP, MP, SR), pp. 146–168.

ILPS-1995-LauOPP #correctness #logic programming #program transformation #termination

Correctness of Logic Program Transformations Based on Existential Termination (KKL, MO, AP, MP), pp. 480–494.

ICLP-1994-ProiettiP #logic

Completeness of Some Transformation Strategies for Avoiding Unnecessary Logical Variables (MP, AP), pp. 714–729.

LOPSTR-1993-ProiettiP #proving #source code #synthesis

Synthesis of Programs from Unfold/Fold Proofs (MP, AP), pp. 141–158.

LOPSTR-1992-ProiettiP #incremental #logic programming #source code

Best-first Strategies for Incremental Transformations of Logic Programs (MP, AP), pp. 82–98.

LOPSTR-1991-ProiettiP #automation #logic programming #source code

An Automatic Transfomation Strategy for Avoiding Unnecessary Variables in Logic Programs (MP, AP), pp. 126–128.

PEPM-1991-ProiettiP #prolog #semantics

Semantics Preserving Transformation Rules for Prolog (MP, AP), pp. 274–284.

PLILP-1991-ProiettiP #logic programming #named #order #source code

Unfolding — Definition — Folding, in this Order, for Avaoiding Unnecessary Variables in Logic Programs (MP, AP), pp. 347–358.

ESOP-1990-ProiettiP #logic programming #source code #synthesis

Synthesis of Eureka Predicates for Developing Logic Programs (MP, AP), pp. 306–325.

LFP-1984-Pettorossi #performance #source code

A Powerful Strategy for Deriving Efficient Programs by Transformation (AP), pp. 273–281.

ICALP-1981-Pettorossi #order #proving #recursion #term rewriting #termination

Comparing and Putting Together Recursive Path Ordering, Simplification Orderings and Non-Ascending Property for Termination Proofs of Term Rewriting Systems (AP), pp. 432–447.

CFLP-1987-PettorossiS #higher-order

Higher Order Generalization in Program Derivation (AP, AS), pp. 182–196.