Gerardo Schneider's Publications: Internal Reports

[1] Raúl Pardo, César Sánchez, and Gerardo Schneider. Timed epistemic knowledge bases for social networks (extended version). Technical Report abs/1708.04070, CoRR - arXiv.org, 2017. [ bib | http ]
[2] John J. Camilleri, Mohammad Reza Haghshenas, and Gerardo Schneider. A web-based tool for analysing normative documents in english. Technical Report abs/1707.03997, CoRR - arXiv.org, 2017. [ bib | http ]
[3] John J. Camilleri, Normunds Gruzitis, and Gerardo Schneider. Extracting formal models from normative texts. Technical Report abs/1607.01485, CoRR - arXiv.org, 2016. [ bib | http ]
[4] Thibaud Antignac, David Sands, and Gerardo Schneider. Data minimisation: A language-based approach (long version). Technical Report abs/1611.05642, CoRR - arXiv.org, 2016. [ bib | http ]
[5] John J. Camilleri, Gabriele Paganelli, and Gerardo Schneider. A CNL for contract-oriented diagrams. Technical Report abs/1406.5691, CoRR - arXiv.org, 2014. [ bib | http ]
[6] Hallstein Hansen, Gerardo Schneider, and Martin Steffen. Reachability analysis of complex planar hybrid systems. Technical Report 412, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, November 2011. [ bib | http | .pdf ]
Hybrid systems are systems that exhibit both discrete and continuous behavior. Reachability, the question of whether a system in one state can reach some other state, is undecidable for hybrid systems in general. The Generalized Polygonal Hybrid System (GSPDI) is a restricted form of hybrid automaton where reachability is decidable. It is limited to two continuous variables that uniquely determine which location the automaton is in, and restricted in that the discrete transitions does not allow changes in the state, only the location, of the automaton. One application of GSPDIs is for approximating control systems and verifying the safety of such systems. In this paper we present the following two contributions: i) An optimized algorithm that answers reachability questions for GSPDIs, where all cycles in the reachability graph are accelerated. ii) An algorithm by which more complex planar hybrid systems are over-approximated by GSPDIs subject to two measures of precision. We prove soundness, completeness, and termination of both algorithms, and discuss their implementation.

[7] Christian Colombo, Gordon Pace, and Gerardo Schneider. Resource-bounded runtime verification of java programs with real-time properties. Technical Report CS2009-01, Department of Computer Science, University of Malta, December 2009. [ bib | .pdf ]
Given the intractability of exhaustively verifying software, the use of runtime verification, to verify single execution paths at runtime, is becoming increasingly popular. Undoubtedly, the overhead introduced by runtime verification is a concern for system developers planning to introduce this technique in their work. By using Lustre to write security-critical properties, we exploit the language's guarantees on bounded resources. We translate these properties into the existing monitoring framework LARVA, making monitoring of programs both easily applicable to Java programs and at the same time guaranteed to use bounded-resources. We use a subset of Quantified Discrete-time Duration Calculus (QDDC) as an alternative specification notation for real-time properties because it is translatable into Lustre. Thus, QDDC also enjoys the same guarantees given when using Lustre.

[8] Gordon J. Pace and Gerardo Schneider. FLACOS'09 Workshop Proceedings. Technical Report 385, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, September 2009. Editors. [ bib | .pdf ]
[9] Gordon J. Pace and Gerardo Schneider. FLACOS'08 Workshop Proceedings. Technical Report 377, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, October 2008. Editors. [ bib | .pdf ]
[10] Cristian Prisacariu and Gerardo Schneider. CL: A Logic for Reasoning about Legal Contracts -Semantics. Technical Report 371, Oslo, Norway, February 2008. [ bib | .pdf ]
The work reported here is concerned with the definition of a logic (which we call CL) for reasoning about legal contracts. The report presents the syntax of the logic and the associated semantics. There are two semantics presented: one is defined with respect to linear structures (i.e. traces of actions) and is intended for run-time monitoring of executions of contracts; the second semantics is given over branching structures (i.e. Kripke-like structures) and is intended for reasoning about contracts in a static manner (i.e. model-checking and theorem proving). In the first part of the report we present the theoretical results underlying the branching semantics. It presents an algebra of actions and restates some of previous results presented in another report, as well as new results useful for the definition of the branching semantics and for the proofs. The rest of the report is concerned with the definition of the two semantics. Moreover, several (non-standard) desired properties of the logic are proven.

[11] Gordon Pace and Gerardo Schneider. Relaxing Goodness is Still Good for SPDIs. Technical Report 372, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, January 2008. [ bib | .pdf ]
Polygonal hybrid systems (SPDIs) are planar hybrid systems, whose dynamics are defined in terms of constant differential inclusions, one for each of a number of polygonal regions partitioning the plane. The reachability problem for SPDIs is known to be decidable, but depends on the goodness assumption - which states that the dynamics do not allow a trajectory to both enter and leave a region through the same edge. In this paper we extend the decidability result to generalised SPDIs (GSPDI), SPDIs not satisfying the goodness property, and give an algorithmic solution to decide reachability of such systems.

[12] Einar B. Johnsen, Olaf Owe, and Gerardo Schneider. NWPT'07/FLACOS'07 Workshop Proceedings. Technical Report 366, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, October 2007. Editors. [ bib | .pdf ]
[13] Olaf Owe, Gerardo Schneider, and Arild Torjusen. Towards integration of XML in the Creol object-oriented language. Technical Report 365, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, October 2007. [ bib | .pdf ]
The integration of XML documents in object-oriented programming languages is becoming paramount with the advent of the use of Internet in new applications like web services. Such an integration is not easy in general and demands a careful language design. In this paper we propose an extension to Creol, a high level object-oriented modeling language for distributed systems, for handling XML documents.

[14] Olaf Owe, Gerardo Schneider, and Martin Steffen. Components, objects, and contracts. Technical Report 363, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, August 2007. [ bib | .pdf ]
Being a composite part of a larger system, a crucial feature of a component is its interface, as it describes the component's interaction with the rest of the system in an abstract manner. It is now commonly accepted that simple, functional interfaces are not expressive enough for components, and the trend is towards behavioral interfaces. We propose to go a step further and enhance components with contracts, i.e., agreements between two or more components on what they are obliged, permitted and forbidden when interacting. This way, contracts are modelled after legal contracts from conventional business or judicial arenas. Indeed, our work aims at a framework for e-contracts, i.e., “electronic” versions of legal documents describing the parties' respective duties. We take the object-oriented, concurrent programming language Creol as starting point and extend it with a notion of components. We then discuss a framework where components are accompanied by contracts and we sketch some ideas on how analysis of compatibility and compositionality could be done in such a setting.

[15] Gordon Pace, Cristian Prisacariu, and Gerardo Schneider. Model checking contracts -a case study. Technical Report 362, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, August 2007. [ bib | .pdf ]
Contracts are agreements between distinct parties that determine rights and obligations on their signatories, and have been introduced in order to reduce risks and to regulate inter-business relationships. In this paper we show how a conventional contract can be written in the contract language CL, how to model the contract, and finally how to verify properties of the model using the NuSMV model checking tool.

[16] Cristian Prisacariu and Gerardo Schneider. An Algebraic Structure for the Action-Based Contract Language CL - theoretical results. Technical Report 361, Department of Informatics, University of Oslo, Oslo, Norway, July 2007. Updated March 2008. [ bib | .pdf ]
We introduce in this paper an algebra of actions specially tailored to serve as basis of an action-based formalism for writing electronic contracts. The proposed algebra is based on the work on Kleene algebras but does not consider the Kleene star and introduces a new constructor for modelling concurrent actions. The algebraic structure is resource-aware and incorporates special actions called tests. In order to be in accordance with the intuition behind electronic contracts we consider new properties of the algebraic structure, in particular a conflict relation and a demanding partial order. We also study a canonical form of the actions which, among other things, helps to naturally define a notion of action negation. Our action negation is more general than just negation of atomic actions, but more restricted than the negation involving the universal relation. A standard interpretation of the algebra is given in terms of guarded rooted trees with specially defined operations on them. The algebra is proven to be complete over the standard interpretation.

Keywords: Electronic contracts, Kleene algebra, guarded rooted trees, concurrency, completeness
[17] Gerardo Schneider. On the decidability of the reachability problem for GSPDIs. Technical Report 359, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, June 2007. [ bib | .pdf ]
Polygonal hybrid systems (SPDIs) are a subclass of hybrid systems whose dynamics is defined by constant differential inclusions, for which the reachability problem is decidable. The decidability result is based, among other things, on the fact that a trajectory cannot enter and leave a given region through the same edge. An SPDI satisfying the above restriction is said to have the goodness property. In a previous work we have given an incomplete proof of decidability of reachability for SPDIs when relaxing goodness. In this work we give a counter-example to such proof and we give an algorithm for semi-deciding reachability of such class of systems.

[18] Cristian Prisacariu and Gerardo Schneider. Towards a formal definition of electronic contracts. Technical Report 348, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, January 2007. [ bib | .pdf ]
In this technical report we discuss the main problems arising when defining a language for contracts. We propose a formal language for writing electronic contracts, based on the deontic notions of obligation, prohibition, and permission. We take an ought-to-do approach, where deontic operators are applied to actions instead of state-of-affairs. We propose an extension of the μ-calculus in order to capture the intuitive meaning of the deontic notions, and to express deterministic and concurrent actions. We provide a translation of the contract language into the logic, and show how the semantics faithfully captures the meaning of the contract language. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as that it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example.

[19] Gordon Pace and Gerardo Schneider. Static analysis of SPDIs for state-space reduction. Technical Report 336, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, April 2006. [ bib | .pdf ]
Polygonal hybrid systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as the computation of certain objects of the phase portrait, namely the viability, controllability and invariance kernels, for such systems is decidable. In this paper we show how to compute another object of an SPDI phase portrait, namely semi-separatrix curves and show how the phase portrait can be used for reducing the state-space for optimizing the reachability analysis.

[20] Pablo Giambiagi, Olaf Owe, Anders P. Ravn, and Gerardo Schneider. Contract-based internet service software development: A proposal. Technical Report 333, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, January 2006. [ bib | .pdf ]
The fast evolution of the Internet has popularized service-oriented architectures dynamic IT-supported inter-business collaborations. Yet, interoperability between different organizations, requires contracts to reduce risks. Thus, high-level models of contracts are making their way into service-oriented architectures, but application developers are still left to their own devices when it comes to writing code that will comply with a contract. This paper surveys existing and proposes new language-based solutions to the above problem. Contracts are formalized as behavioral interfaces, and abstraction mechanisms may guide the developer in the production of contract-aware applications. We concentrate on contracts dealing with performance (real-time) and information flow (confidentiality).

[21] Gerardo Schneider. Towards computing phase portrait objects of polygonal hybrid systems on surfaces. Technical Report 331, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway, March 2005. [ bib | .pdf ]
Polygonal hybrid systems (SPDIs) are a subclass of hybrid systems whose dynamics is defined by constant differential inclusions. We can define SPDIs on surfaces, obtaining a new class of hybrid systems. In this paper we define and compute various phase portrait objects of this new class: invariance, controllability and viability kernels and separatrix sets.

[22] Gerardo Schneider. A constraint-based algorithm for analysing memory usage on java cards. Technical Report RR-5440, INRIA, December 2004. [ bib | .ps.gz ]
We address in this paper the problem of statically determining whether a JavaCard applet may produce a memory overflow because of the dynamic instantiation of classes inside cycles. We provide a constraint-based algorithm which determines potential loops and (mutually) recursive methods. The algorithm operates on the byte-code of an applet. It is written as a set of rules -one for each byte-code instruction- which allows a compositional reasoning and it comprises both inter- and intra-procedural analysis. We aimed at an algorithm suitable to be fed into the proof assistant Coq in order to extract a certified memory usage analyser. We prove termination of the algorithm as well as its soundness and completeness with respect to an abstraction of the operational semantics of the language.

[23] Michael Baldamus, Richard Mayr, and Gerardo Schneider. A backward/forward strategy for verifying safety properties of infinite-state systems. Technical Report 2003-065, Department of Information Technology, Uppsala University, January 2004. [ bib | .pdf ]
This paper has two main contributions: For one, we describe a general method for verifying safety properties of non-well-quasi-ordered infinite-state systems for which reachability is undecidable in general, the question being whether a set U of configurations is reachable. In many cases this problem can be solved as follows: First, one constructs a well-quasi-ordered overapproximation of the system in question. Thereby one can compute an overapproximation of the set Pre*(U) of all predecessors of U. Second, one performs an exact bounded forward search for U (starting at the initial state) which always stays inside the already computed overapproximation of Pre*(U), thus curbing the search space. This restricted forward search is more efficient than a normal forward search, yielding answers of the form YES, NO, or UNKNOWN, where the YES and NO answers are always correct. As our second main contribution herein, we apply our method to relabelling-free CCS with finite sums, which is already a process calculus for which reachability is undecidable. To our knowledge, this part is actually the first application of well-structered systems to verifying safety properties in process calculi. The application is done via a special Petri nets semantics for the calculus that we consider.

[24] Pablo Giambiagi, Gerardo Schneider, and Frank D. Valencia. On the expressiveness of CCS-like calculi. Technical Report 2004-002, Department of Information Technology, Uppsala University, Sweden, January 2004. [ bib | .ps.gz ]
This an extended version of the FOSSACS 2004 paper.

[25] Gerardo Schneider. Invariance kernels of polygonal differential inclusions. Technical Report 2003-042, Department of Information Technology, Uppsala University, August 2003. [ bib | .ps.gz ]
This is the technical report corresponding to the journal paper "Computing invariance kernels of polygonal hybrid systems".

[26] Eugene Asarin, Gerardo Schneider, and Sergio Yovine. On the decidability of the reachability problem for planar differential inclusions. Technical report, VERIMAG, Grenoble, France, January 2001. [ bib | .ps.gz ]
This is an extended version of the HSCC'2001 paper.

[27] Gerardo Schneider and Xu Qiwen. Towards an Operational Semantics of Verilog. Technical Report 147, UNU/IIST, P.O.Box 3058, Macau, October 1998. [ bib | .ps.gz ]
We give an operational semantics of V-, a simple version of Verilog hardware description language.. The language is simple enough for experimenting formalisation, but contains sufficient features for being practically relevant. V- programs can exhibit a rich variety of computations that justifies the introduction of labels in the transition relation to represent the execution of components, time passing and passive transitions. The semantics is compositional and can be used as the formal basis of a formal theory of Verilog.

[28] Pablo Giambiagi and Gerardo Schneider. A Verilog specification of STARI. Technical report, UNU/IIST, P.O.Box 3058, Macau, February 1998. [ bib | .ps.gz ]
Verilog is a Hardware Description Language used for the design and description of hardware in a behavioral and structural way. It has some interesting features like concurrency, synchronism, shared variables, non-blocking assignments (scheduled assignments), timing controls, infinite computations, zero-time computations, etc., that makes it an interesting language to study. This report explains some features of Verilog in an informal way through small examples and presents the Verilog code of STARI as a main application.

[29] Gerardo Schneider and Xu Qiwen. Towards a Formal Semantics of Verilog using Duration Calculus. Technical Report 133, UNU/IIST, P.O.Box 3058, Macau, February 1998. [ bib | .ps.gz ]
Verilog is a Hardware Description Language used for the design and description of hardware in a behavioral and structural way. The meaning of a Verilog program is given by a simulation semantics, which is based on events and lack the necessary formality. Clearly it would be desirable to have a logical formal semantics to reason about properties of Verilog programs and to prove, among other things, the equivalence between programs (specification and implementation). Verilog has some interesting features like concurrency, synchronism, shared variables, non-blocking assignments (scheduled assignments), timing controls, infinite computations, zero-time computations, etc., that makes it an interesting language to study. WDC (Duration Calculus with Weakly Monotonic Time), introduced by Pandya and Dang, seems to provide an appropriate semantical framework for formalising languages with zero-time delays and computations. We introduce a fixed point operator and infinite intervals in WDC obtaining MWDCI. We use MWDCI to give a compositional abstract semantics to the V- subset of Verilog and in particular the fixed point operator is used to give semantics to the loop statements modelling infinite computation taking zero time (infinite in the discrete time) as well as infinite computation in the macro-time. We prove some results (at the semantical level) about the fixed point operator.

[30] Gerardo Schneider. Fixed point theory in Computer Science. Technical report, CPGCC da UFRGS, Porto Alegre, Brazil, January 1995. (In Portuguese). [ bib ]
[31] Gerardo Schneider. An algebraic specification language. Technical report, CPGCC da UFRGS, Porto Alegre, Brazil, July 1994. (In Portuguese). [ bib ]
[32] Gerardo Schneider. Using induction for algorithm design. Technical report, Dissertation for Engineering Degree. Facultad Regional Concepción del Uruguay - UTN, Concepción del Uruguay, Argentina, December 1992. (In Spanish). [ bib ]

This file was generated by bibtex2html 1.97.