@inproceedings{STTES_PreemptionAbstraction_FMICS09,
  author = {Schierboom Erik and Tamalet, Alejandro and Tews, Hendrik and
              van Eekelen, Marko and Smetsers, Sjaak},
  title = {Preepmtion Abstraction: A Lightweight Approach to Modelling Concurrency},
  booktitle = {Formal Methods for Industrial Critical Systems (FMICS 2009)},
  editor = {Mar\'{\i}a Alpuente and
                 Byron Cook and
                 Christophe Joubert},
  series = {LNCS},
  volume = {5825},
  pages = {149--164},
  year = {2009},
  publisher = {Springer},
  isbn = {978-3-642-04569-1},
  abstract = {This paper presents the preemption abstraction, an abstraction 
technique for lightweight verification of one sequential component of a 
concurrent system. Thereby, different components of the system are permitted
to interfere with each other. The preemption abstraction yields a sequential
abstract system that can easily be described in the higher-order logic of
a theorem prover. One can therefore avoid the cumbersome and costly reasoning
about all possible interleavings of state changes of each system
component. The preemption abstraction is best suited for
components that use preemption points, that is, where the
concurrently running environment can only interfere at a
limited number of points.

The preemption abstraction has been used to model the IPC subsystem of the
Fiasco microkernel. We proved two practically relevant properties of the model.
On the attempt to prove a third property, namely that the assertions in the code
are always valid, we discovered a bug that could potentially crash the whole
system.}
}

@techreport{inifl2008,
  author = {Alejandro Tamalet and Olha Shkaravska and Marko van Eekelen},
  title = {Non-monotonic Polynomial Size Bounds for Functional Programs},
  editor = {Sven-Bodo Scholz},
  booktitle = {{Proceedings of the 20th Symposium on Implementation and Application of Functional Languages, IFL 2008}},
  number = {Technical Report 274},
  month = {Sept. 10-12},
  institution = {Hartfield, Hertfordshire, UK, Published by the School of Computer Science, University of Hertfordshire, UK},
  year = {2008},
  pages = {145-148},
  research_group = {ds},
  class = {Report}
}

@inproceedings{SET_CollectedSizeSem_IFL09,
  author = {Shkaravska, Olha and van Eekelen, Marko and Tamalet, Alejandro},
  title = {Collected Size Semantics for Functional Programs over Lists},
  booktitle = {Proceedings of the 20th International Symposium on
        the Implementation and Application of Functional Languages (IFL 2008)},
  year = {2008},
  note = {to appear},
  pdfurl = {http://www.cs.ru.nl/~tamalet/downloads/IFL08.pdf},
  abstract = {lists. The collected size semantics of a function definition is
a multivalued size function that collects the dependencies between every
possible output size and the corresponding input sizes.
Such functions annotate standard types and are defined by conditional
rewriting rules generated during type inference.
We focus on the connection between the rewriting rules and lower and upper
bounds on the multivalued size functions, when the bounds are given by piecewise
polynomials. We show how, given a set of conditional rewriting rules,
one can infer bounds that define an indexed family of polynomials
that approximates the multivalued size function.
Using collected size semantics we are able to infer non-monotonic and
non-linear lower and upper polynomial bounds for many functional programs.
As a feasibility study, we use the procedure to infer lower and upper
polynomial size-bounds on typical functions of a list library.}
}

@inproceedings{HT_SecurityAutomata_FASE09,
  author = {Huisman, Marieke and Tamalet, Alejandro},
  title = {A Formal Connection between Security Automata and JML Annotations},
  booktitle = {Fundamental Approaches to Software Engineering (FASE 2009)},
  publisher = {Springer},
  series = {LNCS},
  volume = {5503},
  year = {2009},
  isbn = {978-3-642-00592-3},
  pdfurl = {http://www.cs.ru.nl/~tamalet/downloads/IFL09.pdf},
  abstract = {Security automata are a convenient way to describe security
policies. Their typical use is to monitor the execution of an application,
and to interrupt it as soon as the security policy is violated. However,
run-time adherence checking is not always convenient. Instead, we aim at
developing a technique to verify adherence to a security policy statically.
To do this, we consider a security automaton as specification, and we
generate JML annotations that inline the monitor – as a specification –
into the application. We describe this translation and prove preservation
of program behaviour, i.e., if monitoring does not reveal a security vio-
lation, the generated annotations are respected by the program.
The correctness proofs are formalised using the PVS theorem prover.
This reveals several subtleties to be considered in the definition of the
translation algorithm and in the program requirements.}
}

@techreport{SET_CollectedSizeSemantics_TR,
  author = {Shkaravska, Olha and van Eekelen, Marko and Tamalet, Alejandro},
  title = {Collected Size Semantics for Functional Programs},
  institution = {Radboud University Nijmegen},
  number = {ICIS-R08021},
  month = nov,
  year = {2008},
  pdfurl = {http://www.cs.ru.nl/~tamalet/downloads/CollectedSizeSemanticsTR.pdf},
  abstract = {This work introduces collected size semantics of strict functional
programs over lists. It is presented via non-deterministic numerical functions
annotating types. These functions are defined by conditional rewriting rules
generated during type inference. We focus on the connection between the size
rewriting rules and lower and upper bounds on size dependencies, where the
bounds are given by polynomials extended with the max0-operation. We show how,
given a set of conditional rewriting rules, one can infer bounds that define an
indexed family of max0-polynomials that approximates (from above) the
non-deterministic size dependency.
Using collected size semantics we are able to infer non-monotonic and
non-linear lower and upper bounds for many functional programs. As a
feasibility study we consider the Haskell list library.}
}

@techreport{SET_IndexedFamilies_TR,
  author = {Shkaravska, Olha and van Eekelen, Marko and Tamalet, Alejandro},
  title = {Size Analysis with Indexed Families of $\max_0$-Polynomials.},
  institution = {Radboud University Nijmegen},
  number = {ICIS-R08020},
  month = nov,
  year = {2008},
  pdfurl = {http://www.cs.ru.nl/~tamalet/downloads/IndexedFamilesTR.pdf},
  abstract = {Our previous work studied a size-aware type system for functional
programs with non-monotonic polynomial size dependencies. In that approach output
sizes depended only on input sizes. That is rather restrictive since in many
cases the size of the output can differ for different input data of the same size.
In this paper we remove that limitation by presenting value-sensitive size
dependencies via indexed families of polynomials. When a program has
a family of polynomials as its output-on-input size dependency, then for
each actual input value there is an index such that the corresponding
polynomial in the family precisely defines the size of the output.
We introduce and study a novel size-aware type system in which size
annotations are indexed families of max0-polynomials; max0-polynomials
extend polynomials with the max0-operation to prevent negative sizes.
We prove soundness of the type system and we give several decidability
results for different variants of annotations.}
}

@inproceedings{TSE_AlgebraicDataTypes_TFP08,
  author = {Tamalet, Alejandro and Shkaravska, Olha and van Eekelen, Marko},
  title = {Size Analysis of Algebraic Data Types},
  editor = {Achten, Peter and Koopman, Pieter and Moraz{\'a}n, Marco T.},
  booktitle = {Trends in Functional Programming Volume 9 (TFP'08)},
  pages = {33--48},
  publisher = {Intellect Publishers},
  isbn = {978-1-84150-277-9},
  year = {2009},
  pdfurl = {http://www.cs.ru.nl/~tamalet/downloads/SizeAnalysis.pdf},
  abstract = {We present a size-aware type system for a first-order functional
language with algebraic data types, where types are annotated with polynomials
over size variables. We define how to generate typing rules for each data type,
provided its user defined size function meets certain requirements. As an
example, a program for balancing binary trees is type checked. The type system
is shown to be sound with respect to the operational semantics in the class of
shapely functions. Type checking is shown to be undecidable, however,
decidability for a large subset of programs is guaranteed.}
}

@techreport{TSE_AlgebraicDataTypes_TR,
  author = {Tamalet, Alejandro and Shkaravska, Olha and van Eekelen, Marko},
  title = {A Size-Aware Type System with Algebraic Data Types},
  institution = {Radboud University Nijmegen},
  type = {Technical Report},
  number = {ICIS-R08006},
  month = apr,
  year = {2008},
  pdfurl = {http://www.cs.ru.nl/~tamalet/downloads/SizeAnalysisTR.pdf},
  abstract = {We present a size-aware type system for a first-order functional
language with algebraic data types, where types are annotated with polynomials
over size variables. We define how to generate typing rules for each data type,
provided its user defined size function meets certain requirements. As an
example, a program for balancing binary trees is type checked. The type system
is shown to be sound with respect to the operational semantics in the class of
shapely functions. Type checking is shown to be undecidable, however,
decidability for a large subset of programs is guaranteed.}
}

@mastersthesis{Tamalet_YASPCC_MasterThesis,
  author = {Alejandro Tamalet},
  title = {Yet Another Semantics for Proving Class Correctness},
  school = {Facultad de Ciencias Exactas, Ingenieria y Agrimensura (FCEIA),
              Universidad Nacional de Rosario (UNR)},
  month = apr,
  year = {2006},
  pdfurl = {http://www.cs.ru.nl/~tamalet/downloads/YASPCC.pdf},
  key = {denotational semantics, Eiffel, correctness},
  abstract = {This work is based on a series of papers [9, 10, 11, 12] where
Bertrand Meyer introduces a framework for proving correctness of a subset of
Eiffel programs. They present some novel ideas but they just sketch the
formalism. Some basic definitions like routine calls are flawed and others like
assignments are missing. The work of Blanco and Castro [3] solves many of these
issues and extends the formalism. Our intention is to extend it further,
modeling some concepts in an alternative way and to give more examples of its
use.}
}