# my-publications-Conference.bib

@comment{{This file has been generated by bib2bib 1.97}}

@comment{{Command line: bib2bib -c '$type = "INPROCEEDINGS"' -ob my-publications-Conference.bib my-publications.bib}}  @inproceedings{CRS18wbt, author = {John J. Camilleri and Mohammad Reza Haghshenas and Gerardo Schneider}, title = {{A Web-Based Tool for Analysing Normative Documents in English}}, booktitle = {The 33rd ACM/SIGAPP Symposium On Applied Computing --Software Verification and Testing track (SAC-SVT'18)}, optseries = {SAC'18}, year = {2018}, isbn = {}, location = {Pau, France}, pages = {}, url = {}, doi = {}, publisher = {ACM}, abstract = {Our goal is to use formal methods to analyse normative documents written in English, such as privacy policies and regulations. This requires the combination of a number of different elements, including information extraction from natural language, formal languages for model representation, and an interface for property specification and verification. A number of components for performing these tasks have separately been developed: a natural language extraction tool, a suitable formalism for representing such documents, an interface for building models in this formalism, and methods for answering queries asked of a given model. In this work, each of these concerns is brought together in a web-based tool, providing a single interface for analysing normative texts in English. Through the use of a running example, we describe each component and demonstrate the workflow established by our tool. }, note = {To appear}, pdf = {sac-svt18.pdf} }  @inproceedings{LCC+17pvr, author = {Luteberget, Bj{\o}rnar and Camilleri, John J. and Johansen, Christian and Schneider, Gerardo}, opteditor = {Cimatti, Alessandro and Sirjani, Marjan}, title = {{Participatory Verification of Railway Infrastructure by Representing Regulations in RailCNL}}, booktitle = {15th International Conference on Software Engineering and Formal Methods, (SEFM'17)}, year = {2017}, pages = {87--103}, volume = {10469}, series = {LNCS}, optaddress = {Trento, Italy}, optmonth = {4-8 September}, publisher = {Springer}, abstract = {Designs of railway infrastructure (tracks, signalling and control systems, etc.) need to comply with comprehensive sets of regulations describing safety requirements, engineering conventions, and design heuristics. We have previously worked on automating the verification of railway designs against such regulations, and integrated a verification tool based on Datalog reasoning into the CAD tools of railway engineers. This was used in a pilot project at Norconsult AS (formerly Anacon AS). In order to allow railway engineers with limited logic programming experience to participate in the verification process, in this work we introduce a controlled natural language, RailCNL, which is designed as a middle ground between informal regulations and Datalog code. Phrases in RailCNL correspond closely to those in the regulation texts, and can be translated automatically into the input language of the verifier. We demonstrate a prototype system which, upon detecting regulation violations, traces back from errors in the design through the CNL to the marked-up original text, allowing domain experts to examine the correctness of each translation step and better identify sources of errors. We also describe our design methodology, based on CNL best practices and previous experience with creating verification front-end languages.}, isbn = {978-3-319-66197-1}, doi = {10.1007/978-3-319-66197-1_6}, url = {https://doi.org/10.1007/978-3-319-66197-1_6} }  @inproceedings{AMS17sdv, author = {Antignac, Thibaud and Mukelabai, Mukelabai and Schneider, Gerardo}, title = {{Specification, Design, and Verification of an Accountability-aware Surveillance Protocol}}, booktitle = {The 32nd ACM/SIGAPP Symposium On Applied Computing --Software Verification and Testing track (SAC-SVT'17)}, optseries = {SAC'17}, year = {2017}, isbn = {978-1-4503-4486-9}, location = {Marrakech, Morocco}, pages = {1372--1378}, url = {http://doi.acm.org/10.1145/3019612.3019826}, doi = {10.1145/3019612.3019826}, acmid = {3019826}, publisher = {ACM}, optkeywords = {accountability, formal verification, privacy, protocol}, abstract = {Though controversial, surveillance activities are more and more performed for security reasons. However, such activities are extremely privacy-intrusive. This is seen as a necessary side-effect to ensure the success of such operations. In this paper, we propose an accountability-aware protocol designed for surveillance purposes. It relies on a strong incentive for a surveillance organisation to register its activity to a data protection authority. We first elicit a list of accountability requirements, we provide an architecture showing the interaction of the different involved parties, and we propose an accountability-aware protocol which is formally specified in the applied pi calculus. We use the ProVerif tool to automatically verify that the protocol respects confidentiality, integrity and authentication properties.}, pdf = {sac-svt17.pdf} }  @inproceedings{PPS17sps, author = {Pablo Picazo-S\'anchez and Ra\'ul Pardo and Gerardo Schneider}, title = {{Secure Photo Sharing in Social Networks}}, booktitle = {IFIP Information Security \& Privacy Conference (IFIP SEC'17)}, pages = {79--92}, year = {2017}, opteditor = {Sabrina De Capitani di Vimercati and Fabio Martinelli}, volume = {502}, series = {IFIP Advances in Information and Communication Technology (AICT)}, address = {Rome, Italy}, optmonth = {29-31 May}, publisher = {Springer Science and Business Media}, doi = {10.1007/978-3-319-58469-0_6}, isbn = {978-3-319-58468-3}, e-issn = {}, issn = {18684238}, abstract = {Nowadays, in an ubiquitous world where everything is connected to the Internet and where social networks play an important role in our lives, security and privacy is a must. Billions of pictures are uploaded daily to social networks and, with them, parts of our private life are disclosed. In this work, we propose a practical solution for secure photo sharing on social network with independence of its architecture which can be either centralised or distributed. This solution solves the inconsistencies that appear in distributed social network as a consequence of treating photos and access policies separately. Specifically, we solve this open problem by attaching an access policy to the images and thus, each time a photo is re-shared, the access policy will travel together with the image.}, pdf = {ifip-sec2017-photo_sharing.pdf} }  @inproceedings{TSS17dm, author = {Thibaud Antignac and David Sands and Gerardo Schneider}, title = {{Data Minimisation: A Language-Based Approach}}, booktitle = {IFIP Information Security \& Privacy Conference (IFIP SEC'17)}, pages = {442--456}, year = {2017}, opteditor = {Sabrina De Capitani di Vimercati and Fabio Martinelli}, volume = {502}, series = {IFIP Advances in Information and Communication Technology (AICT)}, address = {Rome, Italy}, optmonth = {29-31 May}, publisher = {Springer Science and Business Media}, doi = {10.1007/978-3-319-58469-0_30}, isbn = {978-3-319-58468-3}, e-issn = {}, issn = {18684238}, abstract = {Data minimisation is a privacy-enhancing principle considered as one of the pillars of personal data regulations. This principle dictates that personal data collected should be no more than necessary for the specific purpose consented by the user. In this paper we study data minimisation from a programming language perspective. We assume that a given program embodies the purpose of data collection, and define a data minimiser as a pre-processor for the input which reduces the amount of information available to the program without compromising its functionality. We give formal definitions, and provide a procedure to synthesise a correct data minimiser for a given program.}, pdf = {ifip-sec17-data_min.pdf} }  @inproceedings{PKS+16sep, author = {Ra\'ul Pardo and Ivana Kelly\'erov\'a and C\'esar S\'anchez and Gerardo Schneider}, title = {{Specification of Evolving Privacy Policies for Online Social Networks}}, booktitle = {23rd International Symposium on Temporal Representation and Reasoning (TIME'16)}, pages = {70--79}, year = {2016}, opteditor = {Curtis E. Dyreson and Michael R. Hansen and Luke Hunsberger}, optvolume = {}, optnumber = {}, optseries = {}, optaddress = {Lyngby, Denmark}, optmonth = {17-19 October}, publisher = {IEEE CPS}, abstract = {Online Social Networks are ubiquitous,bringing not only numerous new possibilities but also big threats and challenges. Privacy is one of them. Most social networks today offer a limited set of (static) privacy settings, not being able to express dynamic policies. For instance, users might decide to protect their location during the night, or share information with difference audiences depending on their current position. In this paper we introduce TFPPF, a formal framework to express, and reason about, dynamic (and recurrent) privacy policies that are activated or deactivated by context (events) or time. Besides a formal policy language (TPPL), the framework includes a knowledge-based logic extended with (linear) temporal operators and a learning modality (TKBL). Policies, and formulae in the logic, are interpreted over (timed) traces representing the evolution of the social network. We prove that checking privacy policy conformance, and the model-checking problem for TKBL, are both decidable.}, doi = {10.1109/TIME.2016.15}, e-issn = {}, isbn = {978-1-5090-3825-1}, issn = {}, pdf = {time2016.pdf} }  @inproceedings{PCP+16aba, author = {Ra\'ul Pardo and Christian Colombo and Gordon Pace and Gerardo Schneider}, title = {{An Automata-based Approach to Evolving Privacy Policies for Social Networks}}, booktitle = {The 16th International Conference on Runtime Verification (RV'16)}, pages = {285--301}, year = {2016}, opteditor = {Yli{\{e}}s Falcone and C{\'{e}}sar S{\'{a}}nchez}, volume = {10012}, series = {LNCS}, optaddress = {Madrid, Spain}, optmonth = {23-30 September}, optorganization = {}, publisher = {Springer}, abstract = {Online Social Networks (OSNs) are ubiquitous, with more than 70\% of Internet users being active users of such networking services. This widespread use of OSNs brings with it big threats and challenges, privacy being one of them. Most OSNs today offer a limited set of (static) privacy settings and do not allow for the definition, even less enforcement, of more dynamic privacy policies. In this paper we are concerned with the specification and enforcement of dynamic (and recurrent) privacy policies that are activated or deactivated by context (events). In particular, we present a novel formalism of policy automata, transition systems where privacy policies may be defined per state. We further propose an approach based on runtime verification techniques to define and enforce such policies. We provide a proof-of-concept implementation for the distributed social network Diaspora, using the runtime verification tool LARVA to synthesise enforcement monitors.}, doi = {10.1007/978-3-319-46982-9_18}, e-issn = {}, isbn = {978-3-319-46981-2}, issn = {}, pdf = {rv2016.pdf} }  @inproceedings{APS16SE2, author = {Wolfgang Ahrendt and Gordon Pace and Gerardo Schneider}, title = {{StaRVOOrS - Episode II, Strengthen and Distribute the Force}}, booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (1); Track: Static and Runtime Verification: Competitors or Friends?}, pages = {402--415}, year = {2016}, opteditor = {Tiziana Margaria and Bernhard Steffen}, volume = {9952}, series = {LNCS}, optaddress = {Corfu, Greece}, month = {10-14 October}, optorganization = {}, publisher = {Springer}, abstract = {Static and runtime techniques for the verification of programs are complementary. They both have their advantages and disadvantages, and a natural question is whether they may be combined in such a way as to get the advantages of both without inheriting too much from their disadvantages. In a previous contribution to ISoLA'12, we have proposed StaRVOOrS (Static and Runtime Verification of Object-Oriented Software'), a unified framework for combining static and runtime verification in order to check data- and control-oriented properties. Returning to ISoLA here, we briefly report on advances since then: a unified specification language for data- and control-oriented properties, a tool for combined static and runtime verification, and experiments. On that basis, we discuss two future research directions to strengthen the power, and broaden the scope, of combined static and runtime verification: (i) to use static analysis techniques to further optimise the runtime monitor, and (ii) to extend the framework to the distributed case.}, doi = {10.1007/978-3-319-47166-2_28}, isbn = {978-3-319-47165-5}, e-issn = {}, issn = {}, pdf = {ISoLA2016-starvoors.pdf} }  @inproceedings{ASS16PAC, author = {Thibaud Antignac and Riccardo Scandariato and Gerardo Schneider}, title = {{A Privacy-Aware Conceptual Model for Handling Personal Data}}, booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (1); Track: Privacy and Security Issues in Information Systems}, pages = {942--957}, year = {2016}, opteditor = {Tiziana Margaria and Bernhard Steffen}, volume = {9952}, series = {LNCS}, optaddress = {Corfu, Greece}, month = {10-14 October}, optorganization = {}, publisher = {Springer}, abstract = {Handling personal data adequately is one of the biggest challenges of our era. Consequently, law and regulations are in the process of being released, like the European General Data Protection Regulation (GDPR), which attempt to deal with these challenging issue early on. The core question motivating this work is how software developers can validate their technical design vis-a-vis the prescriptions of the privacy legislation. In this paper, we outline the technical concepts related to privacy that need to be taken into consideration in a software design. Second, we extend a popular design notation in order to support the privacy concepts illustrated in the previous point. Third, we show how some of the prescriptions of the privacy legislation and standards may be related to a technical design that employs our enriched notation, which would facilitate reasoning about compliance.}, doi = {10.1007/978-3-319-47166-2_65}, isbn = {978-3-319-47165-5}, e-issn = {}, issn = {}, pdf = {isola2016_Security-DFD.pdf} }  @inproceedings{Schneider16SEP, author = {Gerardo Schneider}, title = {{On the Specification and Enforcement of Privacy-Preserving Contractual Agreements}}, booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (2); Track: Runtime Verification and Enforcement, the (industrial) application perspective}, pages = {413--419}, year = {2016}, opteditor = {Tiziana Margaria and Bernhard Steffen}, volume = {9953}, series = {LNCS}, optaddress = {}, month = {10-14 October}, optorganization = {}, publisher = {Springer}, abstract = {We are here concerned with the enforcement at runtime of contractual agreements (e.g., Terms of Service) that respect users' privacy policies. We do not provide a technical solution to the problem but rather give an overview of a framework for such an enforcement, and briefly discuss related work and ideas on how to address part of the framework.}, doi = {10.1007/978-3-319-47169-3_34}, isbn = {978-3-319-47168-6}, e-issn = {}, issn = {}, pdf = {isola2016_RVE-contracts.pdf} }  @inproceedings{PPS16REE, author = {Gordon Pace and Ra\'ul Pardo and Gerardo Schneider}, title = {{On the Runtime Enforcement of Evolving Privacy Policies in Online Social Networks}}, booktitle = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation -- ISoLA'16 (2); Track: Runtime Verification and Enforcement, the (industrial) application perspective}, pages = {407--412}, year = {2016}, opteditor = {Tiziana Margaria and Bernhard Steffen}, volume = {9953}, series = {LNCS}, optaddress = {Corfu, Greece}, month = {10-14 October}, optorganization = {}, publisher = {Springer}, abstract = {Online Social Networks have increased the need to understand well and extend the expressiveness of privacy policies. In particular, the need to be able to define and enforce dynamic (and recurrent) policies that are activated or deactivated by context (events) or timeouts. We propose an automaton-based approach to define and enforce such policies using runtime verification techniques. In this paper we discuss how our proposed solution addresses this problem without focussing on concrete technical details.}, doi = {10.1007/978-3-319-47169-3_33}, isbn = {978-3-319-47168-6}, e-issn = {}, issn = {}, pdf = {isola16-RVE.pdf} }  @inproceedings{CGS16efm, abstract = {\emph{Normative texts} are documents based on the deontic notions of obligation, permission, and prohibition. Our goal is model such texts using the \codiag{} formalism, making them amenable to formal analysis, in particular verifying that a text satisfies properties concerning causality of actions and timing constraints. We present an experimental, semi-automatic aid to bridge the gap between a normative text and its formal representation. Our approach uses dependency trees combined with our own rules and heuristics for extracting the relevant components. The resulting tabular data can then be converted into a C-O Diagram.}, author = {John J.~Camilleri and Normunds Gruzitis and Gerardo Schneider}, booktitle = {21st International Conference on Applications of Natural Language to Information Systems (NLDB'16)}, pages = {403--408}, year = {2016}, doi = {10.1007/978-3-319-41754-7_40}, opteditor = {Elisabeth M{\'{e}}tais and Farid Meziane and Mohamad Saraee and Vijayan Sugumaran and Sunil Vadera}, month = {22-24 June}, publisher = {Springer}, series = {LNCS}, volume = {9612}, title = {{Extracting Formal Models from Normative Texts}} }  @inproceedings{PSS15cpc, abstract = {Defining and characterising conditional permissions has never been easy. Part of the problem, we believe, comes from the fact that there is not one but a whole family of possible deontic operators, all of them distinct and reasonable, that can be labelled as conditional permissions. In this article, rather than disputing the correct interpretation, we revisit a number of different interpretations the term has received in the literature, and propose appropriate formalisations for these interpretations within the context of contract automata.}, author = {Gordon J.~Pace and Fernando Schapachnik and Gerardo Schneider}, booktitle = {The 28th International Conference on Legal Knowledge and Information Systems (JURIX'15)}, doi = {10.3233/978-1-61499-609-5-61}, e-issn = {1879-8314}, isbn = {978-1-61499-608-8}, issn = {0922-6389}, optaddress = {Braga, Portugal}, optmonth = {December 10-11}, pages = {61--70}, pdf = {jurix2015.pdf}, publisher = {{IOS} Press}, series = {Frontiers in Artificial Intelligence and Applications}, title = {{Conditional Permissions in Contracts}}, volume = {279}, year = {2015}, bdsk-url-1 = {http://dx.doi.org/10.3233/978-1-61499-609-5-61} }  @inproceedings{CAP+15stc, abstract = {We present the tool StaRVOOrS (Static and Runtime Verification of Object-Oriented Software), which combines static and runtime verification (RV) of Java programs. The tool automates a framework which uses partial results extracted from static verification to optimise the runtime monitoring process. StaRVOOrs combines the deductive theorem prover KeY and the RV tool LARVA, and uses properties written using the ppDATE specification language which combines the control-flow property language DATE used in LARVA with Hoare triples assigned to states. We demonstrate the effectiveness of the tool by applying it to the electronic purse application Mondex.}, address = {Vienna, Austria}, author = {Jes\'us Mauricio Chimento and Wolfgang Ahrendt and Gordon Pace and Gerardo Schneider}, booktitle = {The 15th International Conference on Runtime Verification (RV'15)}, doi = {10.1007/978-3-319-23820-3_21}, opteditor = {Ezio Bartocci and Rupak Majumdar}, isbn = {978-3-319-23819-7}, issn = {0302-9743}, month = {September 22-25}, pages = {297--305}, pdf = {rv2015.pdf}, publisher = {Springer}, series = {LNCS}, title = {{STARVOORS: A Tool for Combined Static and Runtime Verification of Java}}, volume = {9333}, year = {2015}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-23820-3_21} }  @inproceedings{ACP+15, abstract = {Static verification techniques can verify properties across all executions of a program, but powerful judgements are hard to achieve automatically. In contrast, runtime verification enjoys full automation, but cannot judge future and alternative runs. In this paper we present a novel approach in which data-centric and control-oriented properties may be stated in a single formalism, amenable to both static and dynamic verification techniques. We develop and formalise a specification notation, ppDATE, extending the control-flow property language used in the runtime verification tool LARVA with pre/post-conditions and show how specifications written in this notation can be analysed both using the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-centric aspects. We apply the approach to Mondex, an electronic purse application.}, address = {Oslo, Norway}, author = {Wolfgang Ahrendt and Mauricio Chimento and Gordon Pace and Gerardo Schneider}, booktitle = {Formal Methods (FM'15)}, doi = {10.1007/978-3-319-19249-9_8}, opteditor = {Nikolaj Bj{\o}rner and Frank D. de Boer}, isbn = {978-3-319-19248-2}, issn = {0302-9743}, month = {June 24-26}, pages = {108-125}, pdf = {fm2015.pdf}, publisher = {Springer}, series = {LNCS}, title = {A Specification Language for Static and Runtime Verification of Data and Control Properties}, volume = {9109}, year = {2015}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-19249-9_8} }  @inproceedings{ESS15dpn, abstract = {Differential privacy provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge. Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction. This paper is about a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy (PDP). In PDP each individual has its own personal privacy level. We describe ProPer, a interactive system for implementing PDP which maintains a privacy budget for each individual. When a primitive query is made on data derived from individuals, the provenance of the involved records determines how the privacy budget of an individual is affected: the number of records derived from Alice determines the multiplier for the privacy decrease in Alice's budget. This offers some advantages over previous systems, in particular its fine-grained character allows better utilisation of the privacy budget than mechanisms based purely on the concept of global sensitivity, and it applies naturally to the case of a live database where new individuals are added over time. We provide a formal model of the ProPer approach, prove that it provides personalised differential privacy, and describe a prototype implementation based on McSherry's PINQ system.}, address = {Mumbai, India}, author = {Hamid Ebadi and David Sands and Gerardo Schneider}, booktitle = {Proceedings of the 42nd Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages ({POPL}'15)}, doi = {10.1145/2676726.2677005}, isbn = {978-1-4503-3300-9}, month = {12-18 January}, opteditor = {Sriram K. Rajamani and David Walker}, optorganization = {Tata Institute of Fundamental Research}, pages = {69--81}, pdf = {popl2015.pdf}, publisher = {ACM}, title = {{Differential Privacy: Now it's Getting Personal}}, year = {2015}, bdsk-url-1 = {http://dx.doi.org/10.1145/2676726.2677005} }  @inproceedings{CPS14cnl, abstract = {We present a first step towards a framework for defining and manipulating normative documents or contracts described as Contract-Oriented (C-O) Diagrams.These diagrams provide a visual representation for such texts, giving the possibility to express a signatory's obligations, permissions and prohibitions, with or without timing constraints, as well as the penalties resulting from the non-fulfilment of a contract. This work presents a CNL for verbalising C-O Diagrams, a web-based tool allowing editing in this CNL, and another for visualising and manipulating the diagrams interactively. We then show how these proof-of-concept tools can be used by applying them to a small example.}, author = {John J.~Camilleri and Gabrielle Paganelli and Gerardo Schneider}, booktitle = {Fourth Workshop on Controlled Natural Language (CNL 2014)}, doi = {10.1007/978-3-319-10223-8_13}, isbn = {978-3-319-10222-1}, issn = {0302-9743}, optaddress = {Galway, Ireland}, opteditor = {Brian Davis and Kaarel Kaljurand and Tobias Kuhn}, pages = {135--146}, pdf = {cnl2014.pdf}, publisher = {Springer}, series = {LNCS}, title = {A CNL for Contract-Oriented Diagrams}, volume = {8625}, year = {2014}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-10223-8_13} }  @inproceedings{PS14fpp, abstract = {Social networks (SN) provide a great opportunity to help people interact with each other in different ways depending on the kind of relationship that links them. One of the aims of SN is to be flexible in the way one shares information, being as permissive as possible in how people communicate and disseminate information. While preserving the spirit of SN, users would like to be sure that their privacy is not compromised. One way to do so is by providing users with means to define their own privacy policies and give guarantees that they will be respected. In this paper we present a privacy policy framework for SN, consisting of a formal model of SN, a knowledge-based logic, and a formal privacy policy language. The framework may be tailored by providing suitable instantiations of the different relationships, the events, the propositions representing what is to be known, and the additional facts or rules a particular social network should satisfy. Besides, models of Facebook and Twitter are instantiated in our formalism, and we provide instantiations of a number of richer privacy policies.}, author = {Ra\'ul Pardo and Gerardo Schneider}, booktitle = {12th International Conference on Software Engineering and Formal Methods (SEFM'14)}, doi = {10.1007/978-3-319-10431-7_30}, isbn = {978-3-319-10430-0}, issn = {0302-9743}, optaddress = {Grenoble, France}, opteditor = {D. Giannakopoulou and G. Sala\"um}, optmonth = {September 3-5}, pages = {378--392}, pdf = {sefm2014.pdf}, publisher = {Springer}, series = {LNCS}, title = {A Formal Privacy Policy Framework for Social Networks}, volume = {8702}, year = {2014}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-319-10431-7_30} }  @inproceedings{CRS+13tfm, abstract = {In this paper we report and reflect about the didactic principles underlying our endeavour to write a book on Formal Methods for Software Engineering - Languages, Methods, Application Domains'', and to teach its contents at international summer schools. Target audience for the book are taught master students, possibly striving for a career in industry, and doctoral students in their early years, possibly in search of a suitable topic for their dissertation. We outline ten principles underlying the design of the book, coin a recommendation from each principle, and give appropriate examples. We report about the feedback from participants to the schools and lectures, and relate our principles to other pedagogical suggestions for teaching Formal Methods.}, author = {Antonio Cerone and Markus Roggenbach and Holger Schlingloff and Gerardo Schneider and Siraj Shaikh}, booktitle = {Fun with Formal Methods Workshop}, month = {July}, pdf = {fwfm2013.pdf}, title = {Teaching Formal Methods for Software Engineering - Ten Principles}, year = {2013} }  @inproceedings{RS13moa, abstract = {As of today it is still not clear how and when cloud computing should be used. Developers very often write applications in a way that does not really fit a cloud environment, and in some cases without taking into account how quality attributes (like performance, security or portability) are affected. In this paper we share our experience and observations from adopting cloud computing for an on-premise enterprise application in a context of a small software company. We present experimental results concerning a comparative evaluation (w.r.t. performance and cost) of the behavior of the original system both on-premise and on the Cloud, considering different scenarios in the Cloud.}, address = {Malaga, Spain}, author = {Pavel Rabetski and Gerardo Schneider}, booktitle = {European Conference on Service-Oriented and Cloud Computing (ESOCC'13)}, doi = {10.1007/978-3-642-40651-5_19}, isbn = {978-3-642-40650-8}, issn = {0302-9743}, opteditor = {Kung-Kiu Lau and Winfried Lamersdorf and Ernesto Pimentel}, optmonth = {September 11-13}, pages = {227-241}, pdf = {esocc2013.pdf}, publisher = {Springer}, series = {LNCS}, title = {Migration of an on-premise application to the Cloud: Experience report}, volume = {8135}, year = {2013}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-40651-5_19} }  @inproceedings{NST13atr, abstract = {In this paper we deal with the general topic of verification of real-time graphic systems. In particular we present the Runtime Graphics Verification Framework (RUGVEF), where we combine techniques from runtime verification and image analysis to automate testing of graphic systems. We provide a proof of concept in the form of a case study, where RUGVEF is evaluated in an industrial setting to verify an on-air graphics playout system used by the Swedish Broadcasting Corporation. We report on experimental results from the evaluation, in particular the discovery of five previously unknown defects not been detected before.}, address = {Rome, Italy}, author = {Robert Nagy and Gerardo Schneider and Aram Timofeitchik}, booktitle = {{19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13)}}, doi = {10.1007/978-3-642-36742-7_32}, isbn = {978-3-642-36741-0}, issn = {0302-9743}, opteditor = {N. Piterman and S. Smolka}, pages = {465-479}, pdf = {tacas2013.pdf}, publisher = {Springer}, series = {LNCS}, title = {Automatic Testing of Real-Time Graphics Systems}, volume = {7795}, year = {2013}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-36742-7_32} }  @inproceedings{schneider12tfa, address = {Bertinoro, Italy}, author = {Gerardo Schneider}, booktitle = {6th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'12)}, issn = {2075-2180}, month = {19 September}, optnote = {To appear}, series = {EPTCS}, title = {Towards a Framework for Analyzing Normative Texts in Controlled Natural Language}, year = {2012} }  @inproceedings{APS12uas, abstract = {Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control-centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.}, address = {Heraclion, Crete}, author = {Wolfgang Ahrendt and Gordon J.~Pace and Gerardo Schneider}, booktitle = {5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA'12) - Part I}, doi = {10.1007/978-3-642-34026-0_24}, isbn = {978-3-642-34025-3}, issn = {0302-9743}, month = {15-18 October}, opteditor = {T.~Margaria and B.~Steffen and M.~Merten}, optnote = {Track: Runtime Verification: the application perspective}, pages = {312-326}, pdf = {isola12.pdf}, publisher = {Springer}, series = {LNCS}, title = {{A Unified Approach for Static and Runtime Verification: Framework and Applications}}, volume = {7609}, year = {2012}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-34026-0_24} }  @inproceedings{MRS11fcs, abstract = {In this paper we present a framework to analyze conflicts of contracts written in structured English. A contract that has manually been rewritten in a structured English is automatically translated into a formal language using the Grammatical Framework (GF). In particular we use the contract language CL as a target formal language for this translation. In our framework CL specifications could then be input into the tool CLAN to detect the presence of conflicts (whether there are contradictory obligations, permissions, and prohibitions. We also use GF to get a version in (restricted) English of CL formulae. We discuss the implementation of such a framework.}, address = {M\'alaga, Spain}, author = {Seyed M. Montazeri and Nivir Roy and Gerardo Schneider}, booktitle = {5th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'11)}, doi = {10.4204/EPTCS.68.6}, issn = {2075-2180}, month = {22-23 September}, pages = {55-69}, pdf = {flacos11-GFCL.pdf}, series = {EPTCS}, title = {{From Contracts in Structured English to CL Specifications}}, volume = {68}, year = {2011}, bdsk-url-1 = {http://dx.doi.org/10.4204/EPTCS.68.6} }  @inproceedings{MCD+11tas, abstract = {C-O Diagrams have been introduced as a means to have a more visual representation of electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as what are the penalties in case of not fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constraints. In this paper we present a formal semantics for C-O Diagrams based on timed automata extended with an ordering of states and edges in order to represent different deontic modalities.}, address = {M\'alaga, Spain}, author = {Enrique Mart\'{i}nez and Mar\'{i}a E. Cambronero and Gregorio D\'{i}az and Gerardo Schneider}, booktitle = {5th International Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'11)}, doi = {10.4204/EPTCS.68.3}, issn = {2075-2180}, month = {22-23 September}, pages = {7-21}, pdf = {flacos11-CO.pdf}, series = {EPTCS}, title = {{Timed Automata Semantics for Visual e-Contracts}}, volume = {68}, year = {2011}, bdsk-url-1 = {http://dx.doi.org/10.4204/EPTCS.68.3} }  @inproceedings{HSS11ran, abstract = {Many complex continuous systems are modeled as non-linear autonomous systems, i.e., by a set of differential equations with one independent variable. Exact reachability, i.e., whether a given configuration can be reached by starting from an initial configuration of the system, is undecidable in general, as one needs to know the solution of the system of equations under consideration. In this paper we address the reachability problem of planar autonomous systems approximatively. We use an approximation technique which "hybridizes" the state space in the following way: the original system is partitioned into a finite set of polygonal regions where the dynamics on each region is approximated by constant differential inclusions. Besides proving soundness, completeness, and termination of our algorithm, we present an implementation, and its application into (classical) examples taken from the literature.}, address = {Teheran, Iran}, author = {Hallstein A. Hansen and Gerardo Schneider and Martin Steffen}, booktitle = {Fourth International Conference on Fundamentals of Software Engineering (FSEN'11)}, doi = {10.1007/978-3-642-29320-7_14}, opteditor = {F. Arbab and M. Sirjani}, isbn = {978-3-642-29319-1}, issn = {0302-9743}, month = {20-22 April}, pages = {206-220}, pdf = {fsen2011.pdf}, publisher = {Springer}, series = {LNCS}, title = {{Reachability analysis of non-linear planar autonomous systems}}, volume = {7141}, year = {2012}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-29320-7_14} }  @inproceedings{MS10avs, abstract = {In this paper we propose a framework where the behaviour of features can be modelled using a visual model language for contracts (C-O Diagrams). We present a partial translation from C-O Diagrams into the deontic contract language CL allowing to detect whether there are contradicting features, using the tool CLAN. We aim at handling conflicts arising from software evolution and variability. As a proof of concept we apply our technique to a trading system case study.}, author = {Enrique Martinez and Gerardo Schneider}, booktitle = {SPLC Workshops -- 1st International Workshop on Formal Methods in Software Product Line Engineering (FMSPLE'10)}, isbn = {978-1-86220-274-0}, month = {September}, optaddress = {Jeju Island, South Korea}, opturl = {http://dx.doi.org/}, pages = {75-82}, pdf = {FMSPLE10.pdf}, publisher = {Lancaster University}, title = {{Automated Analysis of Conflicts in Software Product Lines}}, volume = {2}, year = {2010} }  @inproceedings{MCD+, abstract = {In a web service composition, an electronic contract (e-contract) regulates how the services participating in the composition should behave, including the restrictions that these services must fulfill, such as real-time constraints. In this work we present a visual model that allows us to specify e-contracts in a user friendly way, including conditional behavior and realtime constraints. A case study is presented to illustrate how this visual model defines e-contracts and a preliminary evaluation of the model is also done.}, address = {Los Alamitos, USA}, author = {Enrique Martinez and Emilia Cambronero and Gregorio Diaz and Gerardo Schneider}, booktitle = {The 7th IEEE International Conference on Services Computing (IEEE SCC'10)}, doi = {10.1109/SCC.2010.32}, isbn = {978-0-7695-4126-6}, month = {July 5-10}, pages = {1--8}, pdf = {scc2010.pdf}, publisher = {IEEE Computer Society}, title = {{A Model for Visual Specification of e-Contracts}}, year = {2010}, bdsk-url-1 = {http://dx.doi.org/10.1109/SCC.2010.32} }  @inproceedings{HS10rag, abstract = {Analysis of systems containing both discrete and continuous dynamics, hybrid systems, is a difficult issue. Most problems have been shown to be undecidable, with the exception of a few classes where the dynamics are restricted and/or the dimension is low. In this paper we present some theoretical results concerning the decidability of the reachability problem for a class of planar hybrid systems called Generalized Polygonal Hybrid Systems (GSPDI). These new results provide means to optimize a previous reachability algorithm, making the implementation feasible. We also discuss the implementation of the algorithm into a tool.}, address = {Sierre, Switzerland}, author = {Hallstein A. Hansen and Gerardo Schneider}, booktitle = {25th Annual ACM Symposium on Applied Computing --Software Verification and Testing track (SAC-SVT'10)}, doi = {10.1145/1774088.1774609}, isbn = {978-1-60558-639-7}, month = {March 22-26}, opteditor = {Sung Y. Shin and Sascha Ossowski and Michael Schumacher and Mathew J. Palakal and Chih-Cheng Hung}, pages = {2511-2516}, pdf = {sac10.pdf}, publisher = {ACM}, title = {{Reachability Analysis of GSPDIs: Theory, Optimization, and Implementation}}, year = {2010}, bdsk-url-1 = {http://dx.doi.org/10.1145/1774088.1774609} }  @inproceedings{FPS09ctc, abstract = {As Service-Oriented Architectures are more widely adopted, it becomes more important to adopt measures for ensuring that the services satisfy functional and non-functional requirements. One approach is the use of contracts based on deontic logics, expressing obligations, permissions and prohibitions of the different actors. The use of explicit contracts enables various analysis techniques to be used when using services. A challenging aspect is that of service composition, in which the contracts composed together may result in conflicting situations. Especially in a context where services may be dynamically composed, the need for automated techniques to analyse contracts and ensure their soundness are crucial. In this paper, we present CLAN, a tool for automatic analysis of conflicting clauses of contracts written in the contract language CL. We present a small case study of an airline check-in desk illustrating the use of the tool.}, address = {Macao, China}, author = {Stephen Fenech and Gordon J. Pace and Gerardo Schneider}, booktitle = {7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)}, doi = {10.1007/978-3-642-04761-9_8}, isbn = {978-3-642-04760-2}, issn = {0302-9743}, month = {October}, opteditor = {Zhiming Liu and Anders P. Ravn}, pages = {90--96}, pdf = {atva09.pdf}, publisher = {Springer}, series = {LNCS}, title = {CLAN: A Tool for Contract Analysis and Conflict Discovery}, volume = {5799}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-04761-9_8} }  @inproceedings{APSY02svt, abstract = {We present SPeeDI, a tool for reachability analysis of Polygonal Hybrid Systems (SPDIs)}, address = {Copenhagen, Denmark}, author = {Eugene Asarin and Gordon Pace and Gerardo Schneider and Sergio Yovine}, booktitle = {Computer Aided Verification (CAV'02)}, doi = {10.1007/3-540-45657-0_28}, isbn = {978-3-642-03465-7}, issn = {0302-9743}, month = {July}, opteditor = {E. Brinksma and K.G. Larsen}, pages = {354--358}, pdf = {cav2002.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {{SPeeDI}: a verification tool for polygonal hybrid systems}, volume = {2404}, year = {2002}, bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45657-0_28} }  @inproceedings{AS02wgb, abstract = {We revisited decidability of the reachability problem for low dimensional hybrid systems. Even though many attempts have been done to draw the boundary between decidable and undecidable hybrid systems there are still many open problems in between. In this paper we show that the reachability question for some two dimensional hybrid systems are undecidable and that for other 2-dim systems this question remains unanswered, showing that it is as hard as the reachability problem for Piecewise Affine Maps, that is a well known open problem.}, address = {Brno, Czech Republic}, author = {Eugene Asarin and Gerardo Schneider}, booktitle = {13th International Conference on Concurrency Theory (CONCUR'02)}, doi = {10.1007/3-540-45694-5_14}, isbn = {3-540-44043-7}, issn = {0302-9743}, month = {August}, opteditor = {L. Brim and P. Jancar and M. Kretinsky and A. Kucera}, pages = {193--208}, pdf = {concur2002.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Widening the boundary between decidable and undecidable hybrid systems}, volume = {2421}, year = {2002}, bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45694-5_14} }  @inproceedings{ASY01drp, abstract = { In this paper we develop an algorithm for solving the reachability problem of two-dimensional piece-wise rectangular differential inclusions. Our procedure is not based on the computation of the reach-set but rather on the computation of the limit of individual trajectories. A key idea is the use of one-dimensional affine Poincar{\'e} maps for which we can easily compute the fixpoints. As a first step, we show that between any two points linked by an arbitrary trajectory there always exists a trajectory without self-crossings. Thus, solving the reachability problem requires considering only those. We prove that, indeed, there are only finitely many qualitative types'' of those trajectories. The last step consists in giving a decision procedure for each of them. These procedures are essentially based on the analysis of the limits of extreme trajectories. We illustrate our algorithm on a simple model of a swimmer spinning around a whirlpool.}, address = {Rome, Italy}, author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine}, booktitle = {4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01)}, doi = {10.1007/3-540-45351-2_11}, isbn = {3-540-41866-0}, issn = {0302-9743}, number = {2034}, opteditor = {M.D.~di Benedetto and A.~Sangiovanni-Vincentelli}, pages = {89--104}, pdf = {hs2001.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {On the decidability of the reachability problem for planar differential inclusions}, year = {2001}, bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45351-2_11} }  @inproceedings{ASY02tcp, abstract = {Polygonal hybrid systems are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. Here, we study the problem of defining and constructing the phase portrait of such systems. We identify various important elements of it, such as viability and controllability kernels, and propose an algorithm for computing them all. The algorithm is based on a geometric analysis of trajectories.}, address = {Stanford, USA}, author = {Eugene Asarin and Gerardo Schneider and Sergio Yovine}, booktitle = {5th International Workshop on Hybrid Systems: Computation and Control (HSCC'02)}, doi = {10.1007/3-540-45873-5_7}, isbn = {3-540-43321-X}, issn = {0302-9743}, month = {March}, number = {2289}, opteditor = {C.J. Tomlin and M.R. Greenstreet}, pages = {49--61}, pdf = {hs2002.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Towards Computing Phase Portraits of Polygonal Differential Inclusions}, year = {2002}, bdsk-url-1 = {http://dx.doi.org/10.1007/3-540-45873-5_7} }  @inproceedings{BPS05pam, abstract = {Memory consumption policies provide a means to control resource usage on constrained devices, and play an important role in ensuring the overall quality of software systems, and in particular resistance against resource exhaustion attacks. Such memory consumption policies have been previously enforced through static analysis, which yield automatic bounds at the cost of precision, or run-time analysis, which incur an overhead that is not acceptable for constrained devices. In this paper, we study the use of logical methods to specify and statically verify precise memory consumption policies for Java bytecode programs. First, we demonstrate how the Bytecode Specification Language (a variant of the Java Modelling Language tailored to bytecode) can be used to specify precise memory consumption policies for (sequential) Java applets, and how verification tools can be used to enforce such memory consumption policies. Second, we consider the issue of inferring some of the annotations required to express the memory consumption policy, and report on an inference algorithm. Our broad conclusion is that logical methods provide a suitable means to specify and verify expressive memory consumption policies, with an acceptable overhead.}, address = {Koblenz, Germany}, author = {Gilles Barthe and Mariela Pavlova and Gerardo Schneider.}, booktitle = {3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)}, doi = {10.1109/SEFM.2005.34}, isbn = {0-7695-2435-4}, month = {September}, pages = {86--95}, pdf = {sefm2005.pdf}, publisher = {IEEE Computer Society}, title = {Precise analysis of memory consumption using program logics}, year = {2005}, bdsk-url-1 = {http://dx.doi.org/10.1109/SEFM.2005.34} }  @inproceedings{CJPS05cmu, abstract = {We present a certified algorithm for resource usage analysis, applicable to languages in the style of Java byte code. The algorithm verifies that a program executes in bounded memory. The algorithm is destined to be used in the development process of applets and for enhanced byte code verification on embedded devices. We have therefore aimed at a low-complexity algorithm derived from a loop detection algorithm for control flow graphs. The expression of the algorithm as a constraint-based static analysis of the program over simple lattices provides a link with abstract interpretation that allows to state and prove formally the correctness of the analysis with respect to an operational semantics of the program. The certification is based on an abstract interpretation framework implemented in the Coq proof assistant which has been used to provide a complete formalisation and formal verification of all correctness proofs.}, address = {Newcastle Upon Tyne, UK}, author = {David Cachera and Thomas Jensen and David Pichardie and Gerardo Schneider}, booktitle = {Formal Methods (FM'05)}, doi = {10.1007/11526841_8}, isbn = {978-3-540-27882-5}, issn = {0302-9743}, month = {July}, pages = {91--106}, pdf = {fm2005.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Certified memory usage analysis}, volume = {3582}, year = {2005}, bdsk-url-1 = {http://dx.doi.org/10.1007/11526841_8} }  @inproceedings{CPS08lrt, abstract = {Given the intractability of exhaustively verifying software, the use of runtime-verification, to verify single execution paths at runtime, is becoming popular. Although the use of runtime verification is increasing in industrial settings, various challenges still are to be faced to enable it to spread further. We present dynamic communicating automata with timers and events to describe properties of systems, implemented in LARVA, an event-based runtime verification tool for monitoring temporal and contextual properties of Java programs. The combination of timers with dynamic automata enables the straightforward expression of various properties, including replication of properties, as illustrated in the use of LARVA for the runtime monitoring of a real life case study --- an online transaction system for credit card. The features of LARVA are also benchmarked and compared to a number of other runtime verification tools, to assess their respective strengths in property expressivity and overheads induced through monitoring.}, address = {L'Aquila, Italy}, author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider}, booktitle = {{13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'08)}}, doi = {10.1007/978-3-642-03240-0_13}, isbn = {978-3-642-03239-4}, issn = {0302-9743}, month = {September}, pages = {135--149}, pdf = {fmics2008.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties}, volume = {5596}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-03240-0_13} }  @inproceedings{CPS08sir, abstract = {Introducing a monitor on a system typically changes the system's behaviour, whether it is slowing the system down, and increasing memory consumption. This may possibly result in creating bugs not in the original system, or possibly even "fixing" bugs, only to reappear as the monitor is removed. Properties written in a real-time logic, such as duration calculus, can be particularly sensitive to such changes induced through monitoring. In this paper, we identify a class of real-time properties, in duration calculus, which are monotonic under the slowing down (speeding up) of the underlying system. We apply this approach to the real-time runtime monitoring tool LARVA, where we use duration calculus as a monitoring property specification language, so we automatically identify properties which can be shown to be monotonic with respect to system re-timing.}, address = {Budapest, Hungary}, author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider}, booktitle = {The 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09)}, doi = {10.1007/978-3-642-04368-0_10}, opteditor = {Joel Ouaknine and Frits Vaandrager}, isbn = {978-3-642-04367-3}, issn = {0302-9743}, month = {13-16 September}, pages = {103--117}, pdf = {formats2009.pdf}, publisher = {Springer}, series = {LNCS}, title = {Safe Runtime Verification of Real-Time Properties}, volume = {5813}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-04368-0_10} }  @inproceedings{CPS09ltr, abstract = {The use of runtime verification, as a lightweight approach to guarantee properties of systems, has been increasingly employed on real-life software. In this paper, we present a tool LARVA, for the runtime verification of real-time properties of Java programs. Properties can be expressed in a number of notations, including timed-automata enriched with stopwatches, Lustre, and a subset of duration calculus. The tool has been successfully used on a number of case-studies, including an industrial system handling financial transactions. LARVA also performs analysis of real-time properties, to calculate, if possible, an upper-bound on the memory and temporal overheads induced by monitoring. Moreover, it gives other useful information, as for instance what is the impact of monitoring the system with respect to the monitored properties.}, address = {Hanoi, Vietnam}, author = {Christian Colombo and Gordon J. Pace and Gerardo Schneider}, booktitle = {7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09)}, doi = {10.1109/SEFM.2009.13}, isbn = {978-0-7695-3870-9}, month = {23--27 November}, pages = {33--37}, pdf = {sefm2009.pdf}, publisher = {IEEE Computer Society}, title = {{LARVA --- Safer Monitoring of Real-Time Java Programs (Tool Paper)}}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1109/SEFM.2009.13} }  @inproceedings{FOP+08bsc, abstract = {Contracts are specifications of properties of an interface to a software component; in this paper we focus on behavioural properties. We consider the problem of giving a full contract that specifies not only the normal behaviour, but also special cases and tolerated exceptions. We conjecture that operational specifications are well suited for normal cases, but are less easily extended for exceptional cases. Logic based specifications are essentially compositional, helping in some cases the specification of exceptional cases. This hypothesis is investigated by comparing specifications in CSP (operational) with specifications in LTL, CTL and a deontic logic based language CL. The specifications give successive extensions to a contract for a Cash Desk example. The outcome of the experiment supports the conjecture and demonstrates clear differences in the basic descriptive power of the formalisms.}, address = {York, UK}, author = {Stephen Fenech and Joseph Okika and Gordon J. Pace and Anders P. Ravn and Gerardo Schneider}, booktitle = {6th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA'09)}, doi = {10.1016/j.entcs.2009.09.027}, issn = {1571-0661}, month = {March}, number = {1}, pages = {39--55}, pdf = {fesca09-cocome.pdf}, series = {ENTCS}, title = {On the Specification of Full Contracts}, volume = {253}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1016/j.entcs.2009.09.027} }  @inproceedings{FPS09acd, abstract = {Industry is currently pushing towards Service-Oriented Architectures, where code execution is not limited to the organisational borders but may be extended beyond, to sources typically not accessible. Contracts, expressing obligations, permissions and prohibitions of the different actors, can be used to protect the interests of the organisations engaged in such service exchange. The, potentially dynamic, composition of different services with different contracts, and the combination of service contracts with local contracts can give rise to unexpected conflicts, exposing the need for automatic techniques for contract analysis. In this paper we look at automatic analysis techniques for contracts written in the contract language CL. We present a trace semantics of CL suitable for conflict analysis, and a decision procedure for detecting conflicts (together with its proof of soundness, completeness and termination). We also discuss its implementation and look into the applications of the contract analysis approach we present. These techniques are applied to a small case study of an airline check-in desk.}, address = {Kuala Lumpur, Malaysia}, author = {Stephen Fenech and Gordon J. Pace and Gerardo Schneider}, booktitle = {6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09)}, doi = {10.1007/978-3-642-03466-4_13}, isbn = {978-3-642-03465-7}, issn = {0302-9743}, month = {August}, pages = {200--214}, pdf = {ictac09-contracts.pdf}, publisher = {Springer}, series = {LNCS}, title = {{Automatic Conflict Detection on Contracts}}, volume = {5684}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-03466-4_13} }  @inproceedings{GOSR06lbs, abstract = {The fast evolution of the Internet has popularized service-oriented architectures (SOA) with their promise of dynamic IT-supported inter-business collaborations. Yet this popularity does not reflect on the number of actual applications using the architecture. Programming models in use today make a poor match for the distributed, loosely-coupled, document-based nature of SOA. The gap is actually increasing. For example, 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 future directions regarding language-based solutions to the above problem.}, address = {Set\'ubal, Portugal}, author = {Pablo Giambiagi and Olaf Owe and Anders P. Ravn and Gerardo Schneider}, booktitle = {International Conference on Software and Data Technologies (ICSOFT'06)}, isbn = {972-8865-69-4}, month = {September}, opteditor = {Joaquim Filipe and Boris Shishkov and Markus Helfert}, opturl = {http://dx.doi.org/}, pages = {339--344}, pdf = {icsoft2006.pdf}, publisher = {INSTICC Press}, title = {Language-based Support for Service Oriented Architectures: Future Directions}, year = {2006} }  @inproceedings{GS05mca, abstract = {Memory is a scarce resource in Java smart cards. Developers and card suppliers alike would want to make sure, at compile- or load-time, that a Java Card applet will not overflow memory when performing dynamic class instantiations. Although there are good solutions to the general problem, the challenge is still out to produce a static analyser that is certified and could execute on-card. We provide a constraint-based algorithm which determines potential loops and (mutually) recursive methods. The algorithm operates on the bytecode of an applet and is written as a set of rules associating one or more constraints to each bytecode instruction. The rules are designed so that a certified analyser could be extracted from their proof of correctness. By keeping a clear separation between the rules dealing with the inter- and intra-procedural aspects of the analysis we are able to reduce the space-complexity of a previous algorithm.}, address = {Cali, Colombia}, author = {Pablo Giambiagi and Gerardo Schneider}, booktitle = {Proceedings of CLEI'05}, isbn = {958-670-426-2}, month = {October}, optpublisher = {Pontificia Universidad Javeriana Cali}, opturl = {http://dx.doi.org/}, pdf = {clei2005.pdf}, title = {Memory consumption analysis of Java smart cards}, year = {2005} }  @inproceedings{GSV04eib, abstract = {In the literature there are several CCS-like process calculi differing in the constructs for the specification of infinite behavior and in the scoping rules for channel names. In this paper we study various representatives of these calculi based upon both their relative expressiveness and the decidability of \emph{divergence}. We regard any two calculi as being \emph{equally expressive} iff for every process in each calculus, there exists a \emph{weakly bisimilar} process in the other. By providing \emph{weak bisimilarity} preserving mappings among the various variants, we show that in the context of \emph{relabeling-free} and \emph{finite summation} calculi: (1) CCS with \emph{parameterless} (or \emph{constant}) definitions is equally expressive to the variant with \emph{parametric} definitions. (2) The CCS variant with \emph{replication} is equally expressive to that with \emph{recursive expressions} and \emph{static} scoping. We also state that the divergence problem is undecidable for the calculi in (1) but decidable for those in (2). We obtain this from (un)decidability results by Busi, Gabbrielli and Zavattaro, and by showing the relevant mappings to be computable and to preserve divergence and its negation. From (1) and the well-known fact that parametric definitions can replace injective relabelings, we show that injective relabelings are redundant (i.e., derived) in CCS (which has constant definitions only).}, address = {Barcelone, Spain}, author = {Pablo Giambiagi and Gerardo Schneider and Frank D. Valencia}, booktitle = {Foundations of Software Science and Computation Structures (FOSSACS'04)}, doi = {10.1007/978-3-540-24727-2_17}, isbn = {3-540-21298-1}, issn = {0302-9743}, month = {March}, pages = {226--240}, pdf = {fossacs2004.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {On the expressiveness of infinite behavior and name scoping in process calculi}, volume = {2987}, year = {2004}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-24727-2_17} }  @inproceedings{HS07dpc, abstract = {In this paper we propose a more general definition of confidentiality, as an aspect of information security including information flow control. We discuss central aspects of confidentiality and their relation with norms and policies, and we introduce a language, with a deontic flavor, to express such norms and policies. Our language may be regarded as a first step towards a formal specification of security policies for confidentiality. We provide a number of examples of useful norms on confidentiality, and we discuss confidentiality policies from real scenarios.}, address = {Manchester, UK}, author = {Johs H. Hammer and Gerardo Schneider}, booktitle = {3rd International Symposium on Information Assurance and Security (IAS'07)}, doi = {10.1109/IAS.2007.64}, isbn = {0-7695-2876-7}, month = {August}, pages = {337-342}, pdf = {ias2007.pdf}, publisher = {IEEE Computer Society Press}, title = {On the definition and policies of confidentiality}, year = {2007}, bdsk-url-1 = {http://dx.doi.org/10.1109/IAS.2007.64} }  @inproceedings{HS09gta, abstract = {The GSPeeDI tool implements a decision procedure for the reachability analysis of GSPDIs, planar hybrid systems whose dynamics is given by differential inclusions, and that are not restricted by the goodness assumption from previous work on the so-called SPDIs. Unlike SPeeDI (a tool for reachability analysis of SPDI) the underlying analysis of GSPeeDI is based on a breadth-first search algorithm, and it can handle more general systems.}, address = {Kuala Lumpur, Malaysia}, author = {Hallstein A. Hansen and Gerardo Schneider}, booktitle = {6th International Colloquium on Theoretical Aspects of Computing (ICTAC'09)}, doi = {10.1007/978-3-642-03466-4_23}, isbn = {978-3-642-03465-7}, issn = {0302-9743}, month = {August}, pages = {336--342}, pdf = {ictac09-GSPeeDI.pdf}, publisher = {Springer}, series = {LNCS}, title = {{GSPeeDI -- A Verification Tool for Generalized Polygonal Hybrid Systems}}, volume = {5684}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-03466-4_23} }  @inproceedings{JSO06rvc, abstract = {Component based software development techniques are becoming increasingly popular, as they improve the software development process through component reuse. However component based development poses a challenge to software verification: How can we assert the correctness of a black-box component without having access to the internal logic of its implementation? In this paper, we propose an approach to this challenge by validating a component's communication history with respect to a specification of its observable behaviour using runtime verification techniques. For this purpose we present a simple specification language for describing component behaviour in terms of communication protocols, a language extension to support error handling at the communication level, and a prototype tool to monitor components and assert that they satisfy their protocol specification at runtime. The prototype is implemented for Java components, supports multithreaded access to the monitored components, and is demonstrated on two examples.}, address = {Cluj-Napoca, Romania}, author = {Einar B. Johnsen and Gerardo Schneider and {\O}ystein Torget}, booktitle = {IEEE 2nd International Conference on Intelligent Computer Communication and Processing (ICCP'06)}, isbn = {978-973-662-233-5}, month = {September}, opturl = {http://dx.doi.org/}, pages = {161--168}, pdf = {iccp2006.pdf}, publisher = {U.T.Press}, title = {Runtime Validation of Communication Histories}, year = {2006} }  @inproceedings{KPS08tbr, abstract = {Electronic inter-organizational relationships are governed by contracts regulating their interaction. It is necessary to run-time monitor the contracts, as to guarantee their fulfillment as well as the enforcement of penalties in case of violations. The present work shows how to obtain a run-time monitor for contracts written in CL, a specification language that allows writing conditional obligations, permissions and prohibitions. We first give a trace semantics for CL which formalises that a trace fulfills a contract. We show how to obtain, for a given contract, a linear-size alternating B{\"u}chi automaton accepting exactly the traces which fulfill the contract. This automaton is the basis for obtaining a finite state machine which acts as a run-time monitor for CL contracts.}, address = {Seoul, South Korea}, author = {Marcel Kyas and Cristian Prisacariu and Gerardo Schneider}, booktitle = {{6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08)}}, doi = {10.1007/978-3-540-88387-6_34}, isbn = {978-3-540-88386-9}, issn = {0302-9743}, month = {October}, pages = {397--407}, pdf = {atva2008.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Run-time Monitoring of Electronic Contracts}, volume = {5311}, year = {2008}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-88387-6_34} }  @inproceedings{OS08wos, abstract = {Despite the effort of researchers on distributed systems, programming languages, and security, there is still no good solution offering basic constructs for guaranteeing minimal security at the programming language level. In particular, the notion of a wrapper around an object controlling its interaction with the environment has not properly been addressed at the programming language level. This kind of local firewall'' may play two different roles: (1) The untrusted part is the object inside the wrapper; (2) The untrusted part is the environment. In this paper we propose the addition of a language primitive for creating wrapped objects, and sketch a formalization based on a minimal object-oriented language for distributed systems, based on asynchronous communication.}, address = {York, UK}, author = {Olaf Owe and Gerardo Schneider}, booktitle = {6th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA'09)}, doi = {10.1016/j.entcs.2009.09.032}, issn = {1571-0661}, month = {March}, number = {1}, pages = {127--143}, pdf = {fesca09-wrappers.pdf}, series = {ENTCS}, title = {Wrap your Objects Safely}, volume = {253}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1016/j.entcs.2009.09.032} }  @inproceedings{OSS07coc, abstract = {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.}, address = {Dubrovnik, Croatia}, author = {Olaf Owe and Gerardo Schneider and Martin Steffen}, booktitle = {{6th Workshop on Specification And Verification of Component-Based Systems (SAVCBS'07)}}, doi = {10.1145/1292316.1292328}, isbn = {978-1-59593-721-6}, month = {September}, pages = {95--98}, pdf = {savcbs2007.pdf}, series = {ACM Digital Library}, title = {Components, Objects, and Contracts}, year = {2007}, bdsk-url-1 = {http://dx.doi.org/10.1145/1292316.1292328} }  @inproceedings{OST07tix, 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.}, author = {Olaf Owe and Gerardo Schneider and Arild Torjusen}, booktitle = {NIK'07 proceedings}, isbn = {9788251922722}, opturl = {http://dx.doi.org/}, pages = {107--111}, pdf = {nik2007.pdf}, publisher = {Tapir Akademisk Forlag}, title = {{Towards integration of XML in the Creol object-oriented language}}, year = {2007} }  @inproceedings{PPS07mcc, 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 = {Tokyo, Japan}, author = {Gordon Pace and Cristian Prisacariu and Gerardo Schneider}, booktitle = {{5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07)}}, doi = {10.1007/978-3-540-75596-8_8}, isbn = {978-3-540-75595-1}, issn = {0302-9743}, month = {October}, pages = {82--97}, pdf = {atva2007.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Model Checking Contracts --A Case Study}, volume = {4762}, year = {2007}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-75596-8_8} }  @inproceedings{PS04mcp, abstract = {Polygonal hybrid systems are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. Here, we identify and compute an important object of such systems' phase portrait, namely {\em invariance kernels}. An \emph{invariant set} is a set of initial points of trajectories which keep rotating in a cycle forever and the \emph{invariance kernel} is the largest of such sets. We show that this kernel is a non-convex polygon and we give a non-iterative algorithm for computing the coordinates of its vertices and edges. Moreover, we present a breadth-first search algorithm for solving the reachability problem for such systems. Invariance kernels play an important role in the algorithm.}, address = {Venice, Italy}, author = {Gordon Pace and Gerardo Schneider}, booktitle = {5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04)}, doi = {10.1007/978-3-540-24622-0_11}, isbn = {978-3-540-20803-7}, issn = {0302-9743}, month = {December}, number = {2937}, pages = {110--121}, pdf = {vmcai2004.pdf}, publisher = {Springer Verlag}, series = {LNCS}, title = {Model Checking Polygonal Differential Inclusions Using Invariance Kernels}, year = {2003}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-24622-0_11} }  @inproceedings{PS06, 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 = {Paris, France}, author = {Gordon Pace and Gerardo Schneider}, booktitle = {4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06)}, doi = {10.1007/11867340_22}, isbn = {978-3-540-45026-9}, issn = {0302-9743}, month = {September}, pages = {306--321}, pdf = {formats2006.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Static Analysis for State-Space Reduction of Polygonal Hybrid Systems}, volume = {4202}, year = {2006}, bdsk-url-1 = {http://dx.doi.org/10.1007/11867340_22} }  @inproceedings{PS06cap, abstract = {The reachability problem as well as the computation of the phase portrait for polygonal hybrid systems (SPDI) has been shown to be decidable. The existing reachability algorithm is based on the exploitation of topological properties of the plane which are used to accelerate certain kind of cycles. The exponential nature of the algorithm makes the analysis of large systems generally unfeasible. In this paper we present a compositional parallel algorithm for reachability analysis of SPDIs. The parallelization is based on the qualitative information obtained from the phase portrait of an SPDI, in particular the controllability kernel.}, address = {Tunis, Tunisia}, author = {Gordon J. Pace and Gerardo Schneider}, booktitle = {3rd International Colloquium on Theoretical Aspects of Computing (ICTAC'06)}, doi = {10.1007/11921240_12}, isbn = {3-540-48815-4}, issn = {0302-9743}, month = {November}, pages = {168--182}, pdf = {ictac2006.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {A Compositional Algorithm for Parallel Model Checking of Polygonal Hybrid Systems}, volume = {4281}, year = {2006}, bdsk-url-1 = {http://dx.doi.org/10.1007/11921240_12} }  @inproceedings{PS07cvp, abstract = {Hybrid systems combining discrete and continuous dynamics arise as mathematical models of various artificial and natural systems, and as an approximation to complex continuous systems. We present the tool SPeeDI+, that extends SPeeDI (a tool that implements a reachability algorithm for polygonal hybrid systems) with the computation of viability, controllability and invariance kernels.}, address = {Budapest, Hungary}, author = {Gordon Pace and Gerardo Schneider}, booktitle = {{14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)}}, doi = {10.1007/978-3-540-78800-3_25}, isbn = {978-3-540-78799-0}, issn = {0302-9743}, month = {March}, pages = {341--345}, pdf = {tacas2008-tool.pdf}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Computation and Visualisation of Phase Portraits for Model Checking SPDIs}, volume = {4963}, year = {2008}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-78800-3_25} }  @inproceedings{PS07fle, abstract = {In this paper we propose a formal language for writing electronic contracts, based on the deontic notions of obligation, permission, and prohibition. 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 concurrent actions. We provide a translation of the contract language into the logic, the semantics of which faithfully captures the meaning of obligation, permission and prohibition. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example.}, address = {Paphos, Cyprus}, author = {Prisacariu, Cristian and Schneider, Gerardo}, booktitle = {9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'07)}, doi = {10.1007/978-3-540-72952-5_11}, isbn = {978-3-540-72919-8}, issn = {0302-9743}, month = {June}, pages = {174--189}, pdf = {fmoods2007.pdf}, publisher = {Springer}, series = {LNCS}, title = {A Formal Language for Electronic Contracts}, volume = {4468}, year = {2007}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-72952-5_11} }  @inproceedings{PS08csf, abstract = {The complete specification of full contracts ---contracts which include tolerated exceptions, and which enable reasoning about the contracts themselves, can be achieved using a combination of temporal and deontic concepts. In this paper we discuss the challenges in combining deontic and other relevant logics, in particular focusing on operators for choice, obligations over sequences, contrary-to-duty obligations, and how internal and external decisions may be incorporated in an action-based language for specifying contracts. We provide different viable interpretations and approaches for the development of such a sound logic and outline challenges for the future.}, address = {D\"useldorf, Germany}, author = {Gordon J. Pace and Gerardo Schneider}, booktitle = {{Integrated Formal Methods (iFM'09)}}, doi = {10.1007/978-3-642-00255-7_20}, isbn = {978-3-642-00254-0}, issn = {0302-9743}, month = {February}, pages = {292--306}, pdf = {ifm2009.pdf}, series = {LNCS}, title = {Challenges in the Specification of Full Contracts}, volume = {5423}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-00255-7_20} }  @inproceedings{PS08rgs, 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 = {Istanbul, Turkey}, author = {Gordon J. Pace and Gerardo Schneider}, booktitle = {{5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08)}}, doi = {10.1007/978-3-540-85762-4_19}, isbn = {978-3-540-85761-7}, issn = {0302-9743}, month = {September}, opteditor = {J.S.Fitzgerald and A.E. Haxhausen and H. Yenigun}, pages = {274--289}, pdf = {ictac2008.pdf}, series = {LNCS}, title = {Relaxing Goodness is Still Good}, volume = {5160}, year = {2008}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-540-85762-4_19} }  @inproceedings{PS09asl, abstract = {The paper presents an action-based formal language called CL for abstract specification of legal contracts. The purpose of the language is to be used to reason about electronic contracts, and as an abstract language for legal contracts. CL combines the legal notions of obligation, permission, and prohibition from deontic logic with the action modality of propositional dynamic logic. The deontic modalities are applied only over actions, thus following the ought-to-do approach. The language includes a synchrony operator to model actions performed at the same time, and a special complementation operation to encode the violation of obligations. The language has a formal semantics in terms of normative structures, specially defined to capture several natural properties of legal contracts. We focus on the informal discussion of the choices made for designing CL, both syntactically and semantically.}, address = {Barcelona, Spain}, author = {Cristian Prisacariu and Gerardo Schneider}, booktitle = {12th International Conference on Artificial Intelligence and Law (ICAIL'09)}, doi = {10.1145/1568234.1568262}, isbn = {978-1-60558-597-0}, month = {June}, pages = {218--219}, pdf = {icail09.pdf}, publisher = {ACM}, title = {Abstract Specification of Legal Contracts (Research Abstract)}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1145/1568234.1568262} }  @inproceedings{PS09cl, abstract = {This paper presents a new version of the CL contract specification language. CL combines deontic logic with propositional dynamic logic but it applies the modalities exclusively over structured actions. CL features synchronous actions, conflict relation, and an action negation operation. The CL version that we present here is more expressive and has a cleaner semantics than its predecessor. We give a direct semantics for CL in terms of normative structures. We show that CL respects several desired properties from legal contracts and is decidable. We relate this semantics with a trace semantics of CL which we used for run-time monitoring contracts.}, address = {Tokyo, Japan}, author = {Cristian Prisacariu and Gerardo Schneider}, booktitle = {16th Workshop on Logic, Language, Information and Computation (WOLLIC'09)}, doi = {10.1007/978-3-642-02261-6_27}, isbn = {978-3-642-02260-9}, issn = {0302-9743}, month = {June}, pages = {335--349}, pdf = {wollic09.pdf}, publisher = {Springer}, series = {LNCS}, title = {{CL: An Action-based Logic for Reasoning about Contracts}}, volume = {5514}, year = {2009}, bdsk-url-1 = {http://dx.doi.org/10.1007/978-3-642-02261-6_27} }  @inproceedings{SX98tfs, abstract = {We formalise the semantics of$V^-$, a simple version of Verilog hardware description language using an extension of Duration Calculus. 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, and it is therefore necessary to extend
Duration Calculus with several features, including Weakly Monotonic Time,
infinite intervals and fixed point operators. The semantics is compositional
and can be used as the formal basis of a formal theory of Verilog.},
author = {Gerardo Schneider and Xu Qiwen},
booktitle = {5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'98)},
doi = {10.1007/BFb0055355},
isbn = {978-3-540-65003-4},
issn = {0302-9743},
month = {September},
number = {1486},
opteditor = {Anders P. Ravn and Hans Rischel},
pages = {282--293},
pdf = {ftrtft98.pdf},
publisher = {Springer Verlag},
series = {LNCS},
title = {Towards a Formal Semantics of Verilog using Duration Calculus},
year = {1998},
bdsk-url-1 = {http://dx.doi.org/10.1007/BFb0055355}
}

@inproceedings{lafferriere00psr,
abstract = {A well known problem in robotics is the motion planning
problem in the presence of static obstacles.  The trajectory of
the robot must satisfy a linear differential equation as
well as possbile input and state constraints.  In this
paper, we explore the use of symbolic reachability algorithms
to decide whether the motion planning problem is feasible
or not. In the case where it is feasible, it computes a feasible
nominal input profile satisfying all system constraints.  Our algorithm
is based on quantifier elimination techniques in the ordered field of
the reals, which have been recently applied to compute the reachable
space for classes of linear hybrid systems.},
author = {Gerardo Lafferriere and George J. Pappas and Gerardo Schneider and Sergio Yovine},
booktitle = {Proceedings of 8th IEEE Mediterranean Conference on Control and Automation},
month = {July},
opturl = {http://dx.doi.org/},
pdf = {med2000.pdf},
title = {Parameter Synthesis in Robot Motion Planning Using Symbolic Reachability Computation},
year = {2000}
}

@inproceedings{schneider08rag,
abstract = {A polygonal hybrid system (SPDIs) is a planar hybrid system, 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 (the so-called {\it goodness} assumption). SPDIs without such an assumption are called Generalized SPDIs (GSPDIs).
In this paper we show that it is not possible to reduce GSPDI reachability to SPDI reachability. Furthermore, we show that the reachability algorithm for SPDIs can be used to semi-decide GSPDI reachability, for which we give a sound algorithm.},
author = {Gerardo Schneider},
booktitle = {23rd Annual ACM Symposium on Applied Computing --Software Verification track (SAC-SV'08)},
doi = {10.1145/1363686.1363773},
isbn = {978-1-59593-753-7},
month = {March},
pages = {327--332},
pdf = {sac-sv2008.pdf},
publisher = {ACM},
title = {Reachability Analysis of {Generalized Polygonal Hybrid Systems}},
year = {2008},
bdsk-url-1 = {http://dx.doi.org/10.1145/1363686.1363773}
}


This file was generated by bibtex2html 1.97.