- Aalto.fi
- sci.aalto.fi
- cs.aalto.fi
- Viorel Preoteasa
Viorel Preoteasa
2015
- Preoteasa Viorel, Back Ralph-Johan, Eriksson Johannes. Verification and code generation for invariant diagrams in Isabelle. Journal of Logical and Algebraic Methods in Programming, 410(42):19-36, 2015. [More info][Pdf] [BibTeX]
Preferred BibTeX:
@article{
pbe2013,
author = "Preoteasa, Viorel and Back, Ralph-Johan and Eriksson, Johannes",
abstract = "Invariant-based programming is a correct-by-construction programming methodology in which programs are expressed as graphs of situations connected by transitions. Such graphs are called invariant diagrams. The situations correspond to the pre- and postconditions and loop invariants of the program, while the transitions correspond to the program statements. The situations are developed before the transitions, and each transition is verified at the time it is added to the diagram. The correctness conditions for the transitions are derived using Hoare-like rules. In this paper, we present an embedding of invariant diagrams in the higher-order logic framework Isabelle/HOL for both proving the verification conditions in the Isabelle proof assistant, as well as generating code that is operationally consistent with the verification semantics by constructing a proof that the generated code is correct with respect to the situations of the invariant diagram. We describe a mechanic translation of the transitions of an invariant diagram into a collection of mutually recursive functions and an associated correctness theorem stating that the value computed by the functions satisfies the final situation. We show that the proofs of the correctness theorem and the well-foundedness of the recursive functions can be built mechanically. The verification conditions are lemmas in the proofs. The collection of recursive functions is a refinement of the original invariant diagram, and is in a form that can be directly converted to executable code by Isabelle. This allows proof-producing compilation of invariant diagrams into any of the languages supported by Isabelle code generator. We illustrate our approach with a case study, and show that full proof automation can be achieved. This work is a step towards verified compilation of invariant diagrams.",
number = "42",
affiliation = "Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5 A, 20520 Turku, Finland",
il = "no",
eventdetails = "NA",
year = "2015",
title = "Verification and code generation for invariant diagrams in Isabelle",
juforank = "2",
unitcode = "T306-100",
impactfactor = "A1",
publisher = "Elsevier",
journal = "Journal of Logical and Algebraic Methods in Programming",
volume = "410",
kay = "NA",
pages = "19-36",
responsibleauthor = "Preoteasa, Viorel",
doi = "10.1016/j.jlap.2013.09.001",
language = "eng",
keyword = "",
issn = "2352-2208",
flags = "copy",
pdf = "preoteasa-back-eriksson-2013.pdf"
}
2014
- Preoteasa Viorel, Tripakis Stavros. Refinement Calculus of Reactive Systems. In Proceedings of the 14th International Conference on Embedded Software, pages 2:1-2:10, 2014. ACM [More info] [BibTeX]
- Preoteasa Viorel. Refinement algebra with dual operator. Science of Computer Programming, 179-210, 2014. [More info][Pdf] [BibTeX]
Preferred BibTeX:
@inproceedings{
Preoteasa:2014:RCR:2656045.2656068,
author = "Preoteasa, Viorel and Tripakis, Stavros",
isbn = "978-1-4503-3052-7",
series = "EMSOFT '14",
il = "yes",
eventdetails = "International conference on embedded software, EMSOFT2014, 12-17 October, New Delhi, India",
year = "2014",
title = "Refinement Calculus of Reactive Systems",
booktitle = "Proceedings of the 14th International Conference on Embedded Software",
acmid = "2656068",
juforank = "1",
location = "New Delhi, India",
unitcode = "T306-100",
articleno = "2",
impactfactor = "A4",
numpages = "10",
responsibleauthor = "Preoteasa, Viorel and Tripakis, Stavros",
address = "New York, NY, USA",
kay = "NA",
pages = "2:1--2:10",
publisher = "ACM",
doi = "10.1145/2656045.2656068",
language = "eng",
url = "http://doi.acm.org/10.1145/2656045.2656068"
}
Preferred BibTeX:
@article{
preoteasa2013,
author = "Preoteasa, Viorel",
volume = "92",
responsibleauthor = "Preoteasa, Viorel",
issn = "0167-6423",
keyword = "",
language = "eng",
title = "Refinement algebra with dual operator",
journal = "Science of Computer Programming",
publisher = "Elsevier",
pdf = "preoteasa-2013.pdf",
abstract = "Abstract Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We introduce here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of our algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).",
juforank = "2",
affiliation = "Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5 A, 20520 Turku, Finland",
doi = "10.1016/j.scico.2013.07.002",
flags = "copy",
il = "no",
eventdetails = "NA",
year = "2014",
unitcode = "T306-100",
kay = "NA",
impactfactor = "A1",
pages = "179-210"
}
2011
- Back Ralph-Johan, Preoteasa Viorel. Semantics and proof rules of invariant based programs. In Proceedings of the 2011 ACM Symposium on Applied Computing, pages 1658-1665, 2011. ACM [More info][Pdf] [BibTeX]
- Preoteasa Viorel, Back Ralph-Johan. Invariant diagrams with data refinement. Formal Aspects of Computing, 1-29, 2011. [More info][Pdf] [BibTeX]
- Preoteasa Viorel. Algebra of Monotonic Boolean Transformers. In Simao, Adenilso and Morgan, Carroll, editors, Formal Methods, Foundations and Applications. Proceedings of Brazilian Symposium on Formal Methods , volume 7021 of Lecture Notes in Computer Science, pages 140-155, 2011. Springer Berlin Heidelberg [Pdf] [BibTeX]
Preferred BibTeX:
@inproceedings{
back-preoteasa-2011,
author = "Back, Ralph-Johan and Preoteasa, Viorel",
numpages = "8",
publisher = "ACM",
doi = "10.1145/1982185.1982532",
isbn = "978-1-4503-0113-8",
title = "Semantics and proof rules of invariant based programs",
series = "SAC '11",
booktitle = "Proceedings of the 2011 ACM Symposium on Applied Computing",
acmid = "1982532",
abstract = "Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and postconditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. The transitions are verified at the time when they are constructed. The correctness of the program is thus established as part of constructing the program. The program structure in invariant based programs is determined by the information content of the situations, using nested invariant diagrams. The control structure is secondary to the situation structure, and will usually not be well-structured in the classical sense, i.e., it is not necessarily built out of single-entry single-exit program constructs. We study in this paper the semantics and proof rules for invariant-based programs. The total correctness of an invariant diagram is established by proving that each transition preserves the invariants and decreases a global variant. The proof rules for invariant-based programs are shown to be correct and complete with respect to an operational semantics. The proof of correctness and completeness introduces the weakest precondition semantics for invariant diagrams, and uses a special construction, based on well-ordered sets, of the least fixpoint of a monotonic function on a complete lattice. The results presented in this paper have been mechanically verified in the PVS theorem prover.",
flags = "copy",
location = "TaiChung, Taiwan",
year = "2011",
pdf = "back-preoteasa-2011.pdf",
pages = "1658--1665",
address = "New York, NY, USA"
}
Preferred BibTeX:
@article{
preoteasa-back-2011,
author = "Preoteasa, Viorel and Back, Ralph-Johan",
publisher = "Springer London",
doi = "10.1007/s00165-011-0195-2",
keyword = "Computer Science",
title = "Invariant diagrams with data refinement",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
abstract = "Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and post-conditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it to the construction of the classical Deutsch–Schorr–Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover.",
affiliation = "Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5 A, 20520 Turku, Finland",
flags = "copy",
year = "2011",
pdf = "preoteasa-back-2011.pdf",
pages = "1-29"
}
Preferred BibTeX:
@inproceedings{
preoteasa-2011,
editor = "Simao, Adenilso and Morgan, Carroll",
author = "Preoteasa, Viorel",
publisher = "Springer Berlin Heidelberg",
title = "Algebra of Monotonic Boolean Transformers",
series = "Lecture Notes in Computer Science",
booktitle = "Formal Methods, Foundations and Applications. Proceedings of Brazilian Symposium on Formal Methods (SBMF 2011)",
abstract = "Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We introduce here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of our algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).",
volume = "7021",
flags = "copy",
year = "2011",
pdf = "preoteasa-2011.pdf",
pages = "140-155"
}
2009
- Preoteasa Viorel, Back Ralph-Johan. Data Refinement of Invariant Based Programs. pages 143 - 163, 2009. [More info][Pdf] [BibTeX]
- Preoteasa Viorel. Frame rule for mutually recursive procedures manipulating pointers. Theoretical Computer Science, 410(42):4216-4233, 2009. [More info][Pdf] [BibTeX]
Preferred BibTeX:
@inproceedings{
Preoteasa2009143,
author = "Preoteasa, Viorel and Back, Ralph-Johan",
note = "Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009)",
doi = "DOI: 10.1016/j.entcs.2009.12.022",
title = "Data Refinement of Invariant Based Programs",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
abstract = "Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and postconditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it the the construction of the classical Deutsch-Schorr-Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover.",
volume = "259",
flags = "copy",
year = "2009",
keywords = "Mechanical verification",
pdf = "marking-refine2009-final.pdf",
pages = "143 - 163"
}
Preferred BibTeX:
@article{
preoteasa2009,
author = "Preoteasa, Viorel",
publisher = "Elsevier",
doi = "10.1016/j.tcs.2009.05.016",
title = "Frame rule for mutually recursive procedures manipulating pointers",
journal = "{Theoretical Computer Science}",
number = "42",
abstract = "Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove a powerful Hoare total correctness rule for mutually recursive procedures manipulating pointers. The rule combines earlier proof rules for (mutually) recursive procedures with the frame rule for pointer programs. The theory, including the proofs, is implemented in the theorem prover PVS. In this implementation program variables and addresses can store values of almost any type of the theorem prover.",
month = "Sep",
volume = "410",
flags = "copy",
year = "2009",
pdf = "jPreoteasa09-frame.pdf",
pages = "4216-4233"
}
2008
- Back Ralph-Johan, Preoteasa Viorel. Semantics and Proof Rules of Invariant Based Programs. Report 903, TUCS - Turku Centre for Computer Science, 2008. Pdf] [BibTeX]
Preferred BibTeX:
@techreport{
tBaPr08a,
author = "Back, Ralph-Johan and Preoteasa, Viorel",
title = "Semantics and Proof Rules of Invariant Based Programs",
abstract = "Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and postconditions as well as invariants) that could arise during the execution of the algorithm. After that, we identify the transitions between the situations, which will give us the flow of control in the program. The transitions are verified at the time when they are constructed. The correctness of the program is thus established as part of constructing the program. The execution of an invariant diagram may start in any situation and will choose one of the enabled transitions in this situation, to continue to the next situation. In this way, the execution proceeds from situation to situation. Execution terminates when a situation is reached from which there are no enabled transitions. Because the execution could start and terminate in any situation, invariant-based programs can be thought of as multiple entry, multiple exit programs. The transitions may have statements with unbounded nondeterminism, because we allow specification statements in transitions. Invariant based programs are thus a considerable generalization of ordinary structured program statements, and defining their semantics and proof theory provides a challenge that usually does not arise for more traditional programming languages. We study in this paper the semantics and proof rules for invariant-based programs. The total correctness of an invariant diagram is established by proving that each transition preserves the invariants and decreases a global variant. The proof rules for invariant-based programs are shown to be correct and complete with respect to an operational semantics. The results presented in this paper have been mechanically verified in the PVS theorem prover.",
year = "2008",
number = "903",
month = "Jun",
flags = "copy",
address = "Turku, Finland",
pdf = "TR903.pdf",
institution = "{TUCS} - Turku Centre for Computer Science"
}
2006
- Preoteasa Viorel. Mechanical Verification of Mutually Recursive Procedures for Parsing Expressions using Separation Logic. Report 771, TUCS - Turku Centre for Computer Science, 2006. Pdf] [BibTeX]
- Preoteasa Viorel. Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. In Misra, J. and Nipkow, T. and Sekerinski, E., editors, Proceedings of FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, volume 4085 of Lecture Notes in Computer Science, pages 508 - 523, 2006. Springer [Pdf] [BibTeX]
- Preoteasa Viorel. Program Variables -- The Core of Mechanical Reasoning about Imperative Programs. 2006. [BibTeX]
Preferred BibTeX:
@techreport{
tPreoteasa06,
author = "Preoteasa, Viorel",
isbn = "952-12-1732-4",
title = "Mechanical Verification of Mutually Recursive Procedures for Parsing Expressions using Separation Logic",
abstract = "This paper adds support for mutually recursive procedures on top of a predicate transformer semantics of imperative programs with pointers implemented in PVS theorem prover. We define and prove correct a collection of mutually recursive procedures which constructs the parsing tree of an expression generated by a context free grammar. We use separation logic to specify and verify these procedures; the parsing tree is represented in memory using pointers and the specification predicates are defined using separation logic.",
year = "2006",
number = "771",
lab = "Software Construction",
month = "May",
flags = "copy",
address = "Turku, Finland",
pdf = "TR771.pdf",
institution = "{TUCS} - Turku Centre for Computer Science"
}
Preferred BibTeX:
@inproceedings{
inpPr06,
editor = "Misra, J. and Nipkow, T. and Sekerinski, E.",
author = "Preoteasa, Viorel",
publisher = "Springer",
title = "Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic",
series = "Lecture Notes in Computer Science",
booktitle = "Proceedings of FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada",
year = "2006",
lab = "Software Construction",
month = "Aug",
volume = "4085",
flags = "copy",
address = "Berlin / Heidelberg",
abstract = "Using a predicate transformer semantics of programs, we introduce statements for heap operations and separation logic operators for specifying programs that manipulate pointers. We prove consistent Hoare total correctness rules for pointer manipulating statements according to the predicate transformer semantics. We prove the frame rule in the context of a programming language with recursive procedures with value and result parameters and local variables, where program variables and addresses can store values of any type of the theorem prover. The theory, including the proofs, is implemented in the theorem prover PVS.",
pdf = "inpPr06.pdf",
pages = "508 - 523"
}
Preferred BibTeX:
@phdthesis{
thesisPr06,
author = "Preoteasa, Viorel",
school = "Turku Centre for Computer Science",
title = "Program Variables -- The Core of Mechanical Reasoning about Imperative Programs",
abstract = {Imperative programming languages are widely used in practice in most of the software development projects. Examples of such languages include C, C++, C#, Java, Pascal, and many more. This thesis is concerned with reasoning about imperative programs. We study both refinement (the construction of correct programs starting from specifications) and correctness (an already written program is proved correct against a pre, post-condition specification), and we provide theorem prover support for reasoning about programs. Although extensive work has been done in the area of program verification, we are still far from expecting software developers to use it routinely in practice. This is justified by the fact that verification methods are very expensive to use when developing programs. In this thesis, we address some problems that occur when one formalizes the semantics of a programming language for mechanical verification purposes. In order to tackle such issues, we introduce a predicate transformer semantics for an imperative programming language and we give a shallow embedding of it in the PVS theorem prover. We treat local variables, mutually recursive procedures, and pointers. In our embedding, program variables can have any type whose cardinal is bounded by an arbitrary fixed cardinal. For pointers, we use two models: one in which they are modeled as functions from addresses to values, and another one based on separation logic. We propose refinement rules and Hoare total correctness rules for local variables and pointer statements, and also for mutually recursive procedures. The Hoare rules are proved correct with respect to the predicate transformer semantics mentioned above. Various examples show our theory at work. <p> More details about the PVS implementation can be found <a href="../thesis">here</a>.},
month = "November",
flags = "copy",
year = "2006",
pdf = "thesis.pdf",
type = "{PhD} Thesis"
}
2005
- Back Ralph-Johan, Preoteasa Viorel. An Algebraic Treatment of Procedure Refinement to Support Mechanical Verification. Formal Aspects of Computing, 17(1):69-90, 2005. [Pdf] [BibTeX]
Preferred BibTeX:
@article{
artBaPr05a,
author = "Back, Ralph-Johan and Preoteasa, Viorel",
publisher = "Springer",
title = "An Algebraic Treatment of Procedure Refinement to Support Mechanical Verification",
journal = "Formal Aspects of Computing",
address = "Berlin / Heidelberg",
number = "1",
abstract = "We introduce a new algebraic model for program variables, suitable for reasoning about recursive procedures with parameters and local variables in a mechanical verification setting. We give a predicate transformer semantics to recursive procedures and prove refinement rules for introducing recursive procedure calls, procedure parameters, and local variables. We also prove, based on the refinement rules, Hoare total correctness rules for recursive procedures, and parameters. We introduce a special form of Hoare specification statement which alone is enough to fully specify a procedure. Moreover, we prove that this Hoare specification statement is equivalent to a refinement specification. We implemented this theory in the PVS theorem prover.",
month = "May",
volume = "17",
flags = "copy",
year = "2005",
pdf = "jBaPr05a.pdf",
pages = "69-90"
}
2004
- Back Ralph-Johan, Preoteasa Viorel. A Python Specification of the Tkinter Text-Widget. Report 607, TUCS - Turku Centre for Computer Science, 2004. Pdf] [BibTeX]
- Preoteasa Viorel. Refinement of Recursive Procedures with Parameters in PVS. Report 596, TUCS - Turku Centre for Computer Science, 2004. Pdf] [BibTeX]
Preferred BibTeX:
@techreport{
tBaPr04a,
author = "Back, Ralph-Johan and Preoteasa, Viorel",
title = "A Python Specification of the Tkinter Text-Widget",
abstract = "Writing programs means in addition of using a programming language to use libraries of objects or functions. Looking at the documentation of Tkinter Text-widget and trying to use it we have encountered the problem of unspecified consistent behavior of it. In this paper we give an alternative of specifying and documenting a piece of code giving a functional python module that is intended to behave as the original Tkinter Text-widget.",
year = "2004",
number = "607",
flags = "copy",
address = "Turku, Finland",
pdf = "tBaPr04a.pdf",
institution = "{TUCS} - Turku Centre for Computer Science"
}
Preferred BibTeX:
@techreport{
tPreoteasa04a,
author = "Preoteasa, Viorel",
isbn = "952-12-1319-1",
title = "Refinement of Recursive Procedures with Parameters in {PVS}",
abstract = "We present a shallow embedding in PVS of a predicate transformer semantics of an imperative language suitable for reasoning about recursive procedures with parameters and local variables. We use the PVS dependent type mech- anism for implementing program variables of different types. We use an un- interpreted state space and define the program variables behavior by means of certain tree functions that are supposed to satisfy some axioms. Unlike in the implementations mentioned in the literature, we do not need to change the state space when adding local variables or procedure parameters.",
year = "2004",
number = "596",
lab = "Software Construction",
month = "Mar",
flags = "copy",
address = "Turku, Finland",
pdf = "TR596.pdf",
institution = "{TUCS} - Turku Centre for Computer Science"
}
2003
- Back Ralph-Johan, Fan Xiaocong, Preoteasa Viorel. Reasoning about Pointers in Refinement Calculus. In Proceedings of the Tenth Asia-Pacific Software Engineering Conference , 2003. [Pdf] [BibTeX]
- Back Ralph-Johan, Fan Xiaocong, Preoteasa Viorel. Reasoning about Pointers in Refinement Calculus. Report 543, TUCS - Turku Centre for Computer Science, 2003. Pdf] [BibTeX]
- Back Ralph-Johan, Preoteasa Viorel. Reasoning about Recursive Procedures with Parameters. In Proceedings of the 2003 Workshop on Mechanized Reasoning about Languages with Variable Binding, 2003. ACM Press [Pdf] [BibTeX]
- Back Ralph-Johan, Preoteasa Viorel. Reasoning about Recursive Procedures with Parameters. Report 500, TUCS - Turku Centre for Computer Science, 2003. Pdf] [BibTeX]
Preferred BibTeX:
@inproceedings{
inpBaFaPr03a,
author = "Back, Ralph-Johan and Fan, Xiaocong and Preoteasa, Viorel",
title = "Reasoning about Pointers in Refinement Calculus",
booktitle = "Proceedings of the Tenth Asia-Pacific Software Engineering Conference ({APSEC}'03)",
lab = "Software Construction",
month = "Dec",
project = "refinement methods",
flags = "copy",
year = "2003",
pdf = "inpBaFaPr03a.pdf",
abstract = "Pointers are an important programming concept. They are used explicitely or implicitly in many programming languages. In particular, the semantics of object-oriented programming languages rely on pointers. We introduce a semantics for pointer structures. Pointers are seen as indexes and pointer fields are functions from these indexes to values. Using this semantics we turn all pointer operations into simple assignments and then we use refinement calculus techniques to construct a pointer-manipulating program that checks whether or not a single linked list has a loop.We also introduce an induction principle on pointer structures in order to reduce complexity of the proofs."
}
Preferred BibTeX:
@techreport{
tBaX03a,
author = "Back, Ralph-Johan and Fan, Xiaocong and Preoteasa, Viorel",
isbn = "952-12-1198-9",
title = "Reasoning about Pointers in Refinement Calculus",
abstract = "Pointers are an important programming concept. They are used explicitely or implicitly in many programming languages. In particular, the semantics of object-oriented programming languages rely on pointers. We introduce a semantics for pointer structures. Pointers are seen as indexes and pointer fields are functions from these indexes to values. Using this semantics we turn all pointer operations into simple assignments and then we use refinement calculus techniques to construct a pointer-manipulating program that checks whether or not a single linked list has a loop. We also introduce an induction principle on pointer structures in order to reduce complexity of the proofs.",
year = "2003",
number = "543",
month = "Jul",
project = "refinement methods",
flags = "copy",
address = "Turku, Finland",
pdf = "TR543.pdf",
institution = "{TUCS} - Turku Centre for Computer Science"
}
Preferred BibTeX:
@inproceedings{
inpBaPr03a,
author = "Back, Ralph-Johan and Preoteasa, Viorel",
publisher = "{ACM} Press",
title = "Reasoning about Recursive Procedures with Parameters",
booktitle = "Proceedings of the 2003 Workshop on Mechanized Reasoning about Languages with Variable Binding",
year = "2003",
lab = "Software Construction",
month = "Aug",
project = "refinement",
flags = "copy",
address = "New York, {NY}, {USA}",
keywords = "Refinement Calculus, Recursive procedures",
pdf = "inpBaPr03a.pdf",
abstract = "In this paper we extend the model of program variables from the Refinement Calculus [2] in order to be able to reason more algebraically about recursive procedures with parameters and local variables. We extend the meaning of variable substitution or freeness from the syntax to the semantics of program expressions. We give a predicate transformer semantics to recursive procedures with parameters and prove a refinement rule for introduction of recursive procedure calls. We also prove a Hoare total correctness rule for our recursive procedures. These rules have no side conditions and are easier to apply to programs than the ones in the literature. The theory is built having in mind mechanical verification support using theorem provers like PVS [18] or HOL [11]."
}
Preferred BibTeX:
@techreport{
tBaPr03a,
author = "Back, Ralph-Johan and Preoteasa, Viorel",
isbn = "952-12-1104-0",
title = "Reasoning about Recursive Procedures with Parameters",
abstract = "In this paper we extend the model of program variables from the Refinement Calculus [1] in order to be able to reason more algebraically about recursive procedures with parameters and local variables. We extend the meaning of variable substitution or freeness from the syntax to the semantics of program expressions. We give a predicate transformer semantics to recursive procedures with parameters and prove a refinement rule for introduction of recursive procedure calls. We also prove a Hoare total correctness rule for our recursive procedures. These rules have no side conditions and are easier to apply to programs than the ones in the literature. The theory is built having in mind mechanical verification support using theorem provers like PVS [18] or HOL [10].",
year = "2003",
number = "500",
month = "Jan",
project = "refinement",
flags = "copy",
address = "Turku, Finland",
keywords = "Refinement, Recursive procedures, Semantics, Hoare rules",
pdf = "TR500.pdf",
institution = "{TUCS} - Turku Centre for Computer Science"
}
2002
- Back Ralph-Johan, Milovanov Luka, Porres Ivan, Preoteasa Viorel. An Experiment on Extreme Programming and Stepwise Feature Introduction. Report 451, TUCS - Turku Centre for Computer Science, 2002. Pdf] [BibTeX]
- Back Ralph-Johan, Milovanov Luka, Porres Ivan, Preoteasa Viorel. XP as a Framework for Practical Software Engineering Experiments. In Proceedings of the Agile Processes in Software Engineering XP2002 Third International Conference, 2002. [Pdf] [BibTeX]
Preferred BibTeX:
@techreport{
tBaMiPoPr02a,
author = "Back, Ralph-Johan and Milovanov, Luka and Porres, Ivan and Preoteasa, Viorel",
isbn = "952-12-0979-8",
title = "An Experiment on Extreme Programming and Stepwise Feature Introduction",
abstract = "In this paper we describe our first of the series of experiments with Extreme Programming during a summer project. We also discuss how XP can be used as a software process framework for performing practical experiments in software engineering. We show how the main features of XP help to minimize some problem when trying to perform such experiments in university environment.",
year = "2002",
number = "451",
month = "Dec",
flags = "copy",
address = "Turku, Finland",
keywords = "Extreme Programming, Software Engineering Research, Stepwise Feature Introduction, Software Production in a University Environment",
pdf = "TR451.pdf",
institution = "{TUCS} - Turku Centre for Computer Science"
}
Preferred BibTeX:
@inproceedings{
inpBaMiPoPr02a,
author = "Back, Ralph-Johan and Milovanov, Luka and Porres, Ivan and Preoteasa, Viorel",
title = "{XP} as a Framework for Practical Software Engineering Experiments",
booktitle = "Proceedings of the Agile Processes in Software Engineering {XP2002} Third International Conference",
lab = "Software Construction",
month = "May",
project = "software",
flags = "copy",
year = "2002",
keywords = "Extreme Programming, Software Engineering",
pdf = "inpBaMiPoPr02a.pdf",
abstract = "We discuss how Extreme Programming (XP) can be used as the base software development method to perform practical experiments in software engineering. We show how the main features of XP can help us to minimize some of the problems and difficulties that appear when trying to perform such experiments in a university environment. We also discuss the execution and experiences from one experiment studying a new methodology: the Stepwise Feature Introduction."
}
1999
- Preoteasa Viorel. A Relation Between Unambiguous Regulat Expressions and Abstract Data Types. Fundamenta Informaticae, 40(1):53-77, 1999. [Pdf] [BibTeX]
Preferred BibTeX:
@article{
jPreoteasa99a,
author = "Preoteasa, Viorel",
publisher = "{IOS} Press",
title = "A Relation Between Unambiguous Regulat Expressions and Abstract Data Types",
journal = "Fundamenta Informaticae",
number = "1",
abstract = "Using a categorical model of abstract data types, we show, following Kozen's technique [D. C. Kozen, Inform. and Comput. 110 (1994), no. 2, 366--390] and Tarjan's constructions for a deterministic automaton [R. E. Tarjan, J. Assoc. Comput. Mach. 28 (1981), no. 3, 577--593], that if two unambiguous regular expressions define the same regular language, then they represent two isomorphic abstract data types.",
month = "Oct",
volume = "40",
flags = "copy",
year = "1999",
keywords = "abstract data types, categorical model, unambiguous regular expressions, finite automata",
pdf = "jPreoteasa99a.pdf",
pages = "53-77"
}
Latest update 2014-12-16 11:32 EET Maintained by Viorel Preoteasa