@comment{{This file has been generated by bib2bib 1.97}}
@comment{{Command line: bib2bib -c '$type = "TECHREPORT"' -ob my-publications-TechReport.bib my-publications.bib}}
@techreport{PST19ayp,
author = {Pablo Picazo-S\'anchez and Gerardo Schneider and Juan Tapiador},
title = {After You, Please: Browser Extensions Order Attacks and Countermeasures},
institution = {CoRR - arXiv.org},
year = {2019},
archiveprefix = {arXiv},
url = { http://arxiv.org/abs/1908.02205},
number = {abs/1908.02205},
month = {August}
}
@techreport{PAS+18mdm,
author = {Srinivas Pinisetty and
Thibaud Antignac and
David Sands and
Gerardo Schneider},
title = {{Monitoring Data Minimisation}},
institution = {CoRR - arXiv.org},
number = {abs/1801.02484},
year = {2018},
url = {http://arxiv.org/abs/1801.02484},
archiveprefix = {arXiv},
eprint = {1801.02484},
timestamp = {Thu, 01 Feb 2018 19:52:26 +0100},
biburl = {https://dblp.org/rec/bib/journals/corr/abs-1801-02484}
}
@techreport{corrCPS14cnl,
author = {John J. Camilleri and
Gabriele Paganelli and
Gerardo Schneider},
title = {{A {CNL} for Contract-Oriented Diagrams}},
institution = {CoRR - arXiv.org},
number = {abs/1406.5691},
year = {2014},
url = {http://arxiv.org/abs/1406.5691},
archiveprefix = {arXiv},
eprint = {1406.5691},
timestamp = {Wed, 07 Jun 2017 14:40:19 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CamilleriPS14}
}
@techreport{corrCGS16,
author = {John J. Camilleri and
Normunds Gruzitis and
Gerardo Schneider},
title = {{Extracting Formal Models from Normative Texts}},
institution = {CoRR - arXiv.org},
number = {abs/1607.01485},
year = {2016},
url = {http://arxiv.org/abs/1607.01485},
archiveprefix = {arXiv},
eprint = {1607.01485},
timestamp = {Wed, 07 Jun 2017 14:42:00 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CamilleriGS16}
}
@techreport{corrASS16dm,
author = {Thibaud Antignac and
David Sands and
Gerardo Schneider},
title = {{Data Minimisation: A Language-Based Approach (Long Version)}},
institution = {CoRR - arXiv.org},
number = {abs/1611.05642},
year = {2016},
url = {http://arxiv.org/abs/1611.05642},
archiveprefix = {arXiv},
eprint = {1611.05642},
timestamp = {Wed, 07 Jun 2017 14:41:45 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/AntignacSS16}
}
@techreport{corrPSS17tek,
author = {Ra{\'{u}}l Pardo and
C{\'{e}}sar S{\'{a}}nchez and
Gerardo Schneider},
title = {{Timed Epistemic Knowledge Bases for Social Networks (Extended Version)}},
institution = {CoRR - arXiv.org},
number = {abs/1708.04070},
year = {2017},
url = {http://arxiv.org/abs/1708.04070},
archiveprefix = {arXiv},
eprint = {1708.04070},
timestamp = {Tue, 05 Sep 2017 10:03:46 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1708-04070}
}
@techreport{corr/CHS17wbt,
author = {John J. Camilleri and
Mohammad Reza Haghshenas and
Gerardo Schneider},
title = {{A Web-Based Tool for Analysing Normative Documents in English}},
institution = {CoRR - arXiv.org},
number = {abs/1707.03997},
year = {2017},
url = {http://arxiv.org/abs/1707.03997},
archiveprefix = {arXiv},
eprint = {1707.03997},
timestamp = {Sat, 05 Aug 2017 14:56:05 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/CamilleriHS17}
}
@techreport{HSS11racB,
abstract = {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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Hallstein Hansen and Gerardo Schneider and Martin Steffen},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-374-5},
issn = {0806-3036},
month = {November},
number = {412},
pdf = {report-UiO-412.pdf},
title = {Reachability analysis of complex planar hybrid systems},
url = {http://urn.nb.no/URN:NBN:no-29825},
year = {2011},
bdsk-url-1 = {http://urn.nb.no/URN:NBN:no-29825}
}
@techreport{PS09flacos,
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon J. Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-345-1},
issn = {0806-3036},
month = {September},
note = {Editors},
number = {385},
pdf = {report-UiO-385.pdf},
title = {{FLACOS'09 Workshop Proceedings}},
year = {2009}
}
@techreport{CPS09rbr,
abstract = {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.},
author = {Christian Colombo and Gordon Pace and Gerardo Schneider},
institution = {Department of Computer Science, University of Malta},
month = {December},
number = {CS2009-01},
pdf = {report-Malta-CS2009-01.pdf},
title = {Resource-bounded runtime verification of Java programs with real-time properties},
year = {2009}
}
@techreport{ASY01tr,
abstract = {This is an extended version of the HSCC'2001 paper.},
address = {Grenoble, France},
author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine},
institution = {VERIMAG},
month = {January},
ps = {hs2001_ext.ps.gz},
title = {{On the decidability of the reachability problem for planar differential inclusions}},
year = {2001}
}
@techreport{BMS04bfs,
abstract = { 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 $\mathit{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 $\mathit{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.},
author = {Michael Baldamus and Richard Mayr and Gerardo Schneider},
institution = {Department of Information Technology, Uppsala University},
month = {January},
number = {2003-065},
pdf = {tech_rep_2003-065.pdf},
title = {A backward/forward strategy for verifying safety properties of infinite-state systems},
year = {2004}
}
@techreport{GOSR06cbi,
abstract = {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).},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
issn = {0806-3036},
month = {January},
number = {333},
pdf = {report-UiO-333.pdf},
title = {Contract-based Internet Service Software Development: A Proposal},
year = {2006}
}
@techreport{GSV04ecc,
abstract = {This an extended version of the FOSSACS 2004 paper.},
address = {Sweden},
author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia},
institution = {Department of Information Technology, Uppsala University},
month = {January},
number = {2004-002},
ps = {tec_rep_2004-002.ps.gz},
title = {{On the expressiveness of CCS-like calculi}},
year = {2004}
}
@techreport{JOS07nf,
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-324-9},
issn = {0806-3036},
month = {October},
note = {Editors},
number = {366},
pdf = {report-UiO-366.pdf},
title = {{NWPT'07/FLACOS'07 Workshop Proceedings}},
year = {2007}
}
@techreport{OSS07,
abstract = {Being a composite part of a larger system, a crucial feature of a
component is its \emph{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
\emph{behavioral} interfaces.
We propose to go a step further and enhance components with
\emph{contracts}, i.e., agreements between two or more components on what
they are \emph{obliged,} \emph{permitted} and \emph{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 \emph{e-contracts}, i.e., ``electronic'' versions of legal
documents describing the parties' respective duties.
We take the object-oriented, concurrent programming language \emph{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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-321-4},
issn = {0806-3036},
month = {August},
number = {363},
pdf = {report-UiO-363.pdf},
title = {Components, Objects, and Contracts},
year = {2007}
}
@techreport{OST07tr,
abstract = {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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Olaf Owe and Gerardo Schneider and Arild Torjusen},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-323-0},
issn = {0806-3036},
month = {October},
number = {365},
pdf = {report-UiO-365.pdf},
title = {{Towards integration of XML in the Creol object-oriented language}},
year = {2007}
}
@techreport{PPS07TRmcc,
abstract = {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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
issn = {0806-3036},
month = {August},
number = {362},
optisbn = {82-7368-320-6},
optissn = {0806-3036},
pdf = {report-UiO-362.pdf},
title = {Model Checking Contracts --A Case Study},
year = {2007}
}
@techreport{PS06sas,
abstract = {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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-291-9},
issn = {0806-3036},
month = {April},
number = {336},
pdf = {report-UiO-336.pdf},
title = {Static Analysis of {SPDI}s for State-Space Reduction},
year = {2006}
}
@techreport{PS07tfd,
abstract = {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 $\mu$-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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Cristian Prisacariu and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-305-2},
issn = {0806-3036},
month = {January},
number = {348},
pdf = {report-UiO-348.pdf},
title = {Towards a Formal Definition of Electronic Contracts},
year = {2007}
}
@techreport{PS07tr361,
abstract = {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.},
address = {Oslo, Norway},
author = {Prisacariu, Cristian and Schneider, Gerardo},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-319-2},
issn = {0806-3036},
key = {TechRep},
keywords = {Electronic contracts, Kleene algebra, guarded rooted trees, concurrency, completeness},
month = {July},
note = {Updated March 2008},
number = {361},
pages = {64},
pdf = {report-UiO-361.pdf},
publisher = {Department of Informatics, University of Oslo},
title = {An {A}lgebraic {S}tructure for the {A}ction-{B}ased {C}ontract {L}anguage {CL} - theoretical results},
year = 2007
}
@techreport{PS08TRrgs,
abstract = {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 \emph{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 {\em generalised SPDIs} (GSPDI), SPDIs not satisfying the goodness property, and give an algorithmic solution to decide reachability of such systems.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-331-1},
issn = {0806-3036},
month = {January},
number = {372},
pdf = {report-UiO-372.pdf},
title = {{Relaxing Goodness is Still Good for SPDIs}},
year = {2008}
}
@techreport{PS08flacos,
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gordon J. Pace and Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-337-0},
issn = {0806-3036},
month = {October},
note = {Editors},
number = {377},
pdf = {report-UiO-377.pdf},
title = {{FLACOS'08 Workshop Proceedings}},
year = {2008}
}
@techreport{PS08tr371,
abstract = {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.},
address = {Oslo, Norway},
author = {Cristian Prisacariu and Gerardo Schneider},
isbn = {82-7368-330-3},
issn = {0806-3036},
month = {February},
number = {371},
pages = {68},
pdf = {report-UiO-371.pdf},
publisher = {Department of Informatics, University of Oslo},
title = {{CL: A Logic for Reasoning about Legal Contracts ---Semantics}},
year = 2008
}
@techreport{SX98tos,
abstract = {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.},
address = {P.O.Box 3058, Macau},
author = {Gerardo Schneider and Xu Qiwen},
institution = {UNU/IIST},
month = {October},
number = {147},
ps = {report147.ps.gz},
title = {{Towards an Operational Semantics of Verilog}},
year = {1998}
}
@techreport{giambiagi98avs,
abstract = {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.},
address = {P.O.Box 3058, Macau},
author = {Pablo Giambiagi and Gerardo Schneider},
institution = {UNU/IIST},
month = {February},
ps = {stari.ps.gz},
title = {{A Verilog specification of STARI}},
year = {1998}
}
@techreport{schneider03ikp,
abstract = {This is the technical report corresponding to the journal paper "Computing invariance kernels of polygonal hybrid systems".},
author = {Gerardo Schneider},
institution = {Department of Information Technology, Uppsala University},
month = {August},
number = {2003-042},
ps = {tec_rep_2003-042.ps.gz},
title = {Invariance Kernels of Polygonal Differential Inclusions},
year = {2003}
}
@techreport{schneider04cba,
abstract = {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.},
author = {Gerardo Schneider},
institution = {INRIA},
month = {December},
number = {RR-5440},
ps = {RR-5440.ps.gz},
title = {A constraint-based algorithm for analysing memory usage on Java cards},
year = {2004}
}
@techreport{schneider05tcp,
abstract = {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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-286-2},
issn = {0806-3036},
month = {March},
number = {331},
pdf = {report-UiO-331.pdf},
title = {Towards Computing Phase Portrait Objects of Polygonal Hybrid Systems on Surfaces},
year = {2005}
}
@techreport{schneider07drp,
abstract = {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 {\em 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.},
address = {PO Box 1080 Blindern, N-0316 Oslo, Norway},
author = {Gerardo Schneider},
institution = {Department of Informatics, University of Oslo},
isbn = {82-7368-317-6},
issn = {0806-3036},
month = {June},
number = {359},
pdf = {report-UiO-359.pdf},
title = {On the Decidability of the Reachability Problem for {GSPDIs}},
year = {2007}
}
@techreport{schneider92uia,
address = {Concepci\'on del Uruguay, Argentina},
author = {Gerardo Schneider},
institution = {{Dissertation for Engineering Degree. Facultad Regional Concepci\'on del Uruguay - UTN}},
month = {December},
note = {(In Spanish)},
pages = {91},
title = {{Using induction for algorithm design}},
year = {1992}
}
@techreport{schneider94asl,
address = {Porto Alegre, Brazil},
author = {Gerardo Schneider},
institution = {CPGCC da UFRGS},
month = {July},
note = {(In Portuguese)},
pages = {44},
title = {{An algebraic specification language}},
year = {1994}
}
@techreport{schneider95fpt,
address = {Porto Alegre, Brazil},
author = {Gerardo Schneider},
institution = {CPGCC da UFRGS},
month = {January},
note = {(In Portuguese)},
pages = {68},
title = {{Fixed point theory in Computer Science}},
year = {1995}
}
@techreport{schneider98tfs,
abstract = {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.},
address = {P.O.Box 3058, Macau},
author = {Gerardo Schneider and Xu Qiwen},
institution = {UNU/IIST},
month = {February},
number = {133},
ps = {report133.ps.gz},
title = {{Towards a Formal Semantics of Verilog using Duration Calculus}},
year = {1998}
}
This file was generated by bibtex2html 1.97.