BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Cyprus
1 × Germany
1 × Israel
1 × Spain
1 × Sweden
2 × Belgium
2 × Denmark
2 × France
2 × Portugal
4 × United Kingdom
6 × Italy
6 × USA
Collaborated with:
M.Proietti F.Fioravanti V.Senni E.D.Angelis S.Renault A.Skowron K.Lau M.Ornaghi
Talks about:
program (30) logic (19) transform (18) special (9) strategi (6) constraint (5) variabl (5) verif (5) order (5) fold (5)

Person: Alberto Pettorossi

DBLP DBLP: Pettorossi:Alberto

Facilitated 1 volumes:

LOPSTR 2001Ed

Contributed to:

ICLP 20152015
PPDP 20152015
TACAS 20142014
VMCAI 20142014
PEPM 20132013
PEPM 20132014
LOPSTR 20122012
LOPSTR 20112011
ICLP 20102010
LOPSTR 20102010
LOPSTR 20092009
ICLP 20082008
ICLP 20072007
ICLP 20062006
LOPSTR 20052005
PDCL 20042004
PEPM 20042004
LOPSTR 20022002
LOPSTR 20012001
CL 20002000
LOPSTR 20002000
LOPSTR 20002000
ICLP 19991999
LOPSTR 19991999
POPL 19971997
LOPSTR 19961996
ILPS 19951995
ICLP 19941994
LOPSTR 19931993
LOPSTR 19921992
LOPSTR 19911991
PEPM 19911991
PLILP 19911991
ESOP 19901990
LFP 19841984
ICALP 19811981
TAPSOFT, Vol.2: CFLP 19871987

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.