Search by property
This page provides a simple browsing interface for finding entities described by a property and a named value. Other available search interfaces include the page property search, and the ask query builder.
List of results
- Seminar/2022-06-22 + (We present a framework for modelling and v … We present a framework for modelling and verifying epistemic properties over</br>parameterized multi-agent systems that communicate by truthful public</br>announcements. In this framework, the number of agents or the amount of certain</br>resources are parameterized (i.e. not known a priori), and the corresponding</br>verification problem asks whether a given epistemic property is true regardless</br>of the instantiation of the parameters. As in other regular model checking (RMC)</br>techniques, a finite-state automaton is used to specify a parameterized family</br>of systems.</br></br>Parameterized systems might also require an arbitrary number of announcements,</br>leading to the introduction of the so-called iterated public announcement.</br>Although model checking becomes undecidable because of this operator, we provide</br>a semi-decision procedure based on Angluin's L*-algorithm for learning finite</br>automata. Moreover, the procedure is guaranteed to terminate when some</br>regularity properties are met. We illustrate the approach on the Muddy Children</br>puzzle, and we further discuss dynamic protocol encodings through the Dining</br>Cryptographer example.</br></br>Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomasint work with Anthony Lin and Felix Thomas)
- Seminar/2018-05-30 + (We show a symbolic-execution-based algorit … We show a symbolic-execution-based algorithm computing the precise</br>effect of a program cycle on program variables. For a program variable,</br>the algorithm produces an expression representing the variable value</br>after the number of cycle iterations specified by parameters of the</br>expression. The algorithm is partial in the sense that it can fail to</br>find such an expression for some program variables (for example, it</br>fails in cases where the variable value depends on the order of paths in</br>the cycle taken during iterations).</br></br>We present two applications of this loop summarization procedure. The</br>first is the construction of a nontrivial necessary condition on program</br>input to reach a given program location. The second application is a</br>loop bound detection algorithm, which produces tighter loop bounds than</br>other approaches.tighter loop bounds than other approaches.)
- Seminar/2008-04-30 + (Mouldable programming is about looking at … Mouldable programming is about looking at programs as mouldable</br>fragments of code, not as the static, brittle syntax software often</br>turns out to be. Some simple examples follow. The notation for calling</br>a method "push" which adds an element "E" to a stack "S" can be OO or</br>static method style, it can modify "S" or return the new stack</br>etc. Can we simplify usage to just one form, and mould it to the</br>actual call? A function which breaks down for some input can signal</br>this using return flags, special return values, or exceptions, to name</br>some common ways. Can we abstract over this, and mould to the relevant</br>error handling technique? Often we need to do run-time checking of</br>arguments, e.g., array indexing bounds, forcing us to introduce lots</br>of code to deal with the unwanted cases. Can we use mouldable ideas to</br>simplify the code? In the presentation, we will elaborate on such</br>examples, discussing how we can free us from awkward syntactic</br>constraints.ree us from awkward syntactic constraints.)
- Seminar/2012-02-15 + («The effective exploitation of his powers … «The effective exploitation of his powers of abstraction must be</br>regarded as one of the most vital activities of a competent</br>programmer.» disait Dijsktra.</br></br>En effet, pour aborder la complexité d'un problème, l'explicitation</br>des concepts utiles à sa formalisation et à sa résolution est bien</br>souvent une étape clé. Lorsque que l'on étend ce processus à une</br>classe de problèmes qui partagent les mêmes concepts, il est naturel</br>de se doter d'un langage le plus approprié possible pour manipuler ces</br>abstractions spécifiques à un domaine (en anglais, «Domain Specific</br>Language»).</br></br>Comment implémenter ces DSLs? Une première approche classique reflète</br>les constructions du DSL sous la forme d'un jeu de fonctions de</br>bibliothèque. L'avantage de cette approche est d'utiliser directement</br>son langage généraliste préféré, et sa chaîne de compilation</br>optimisée, de façon à générer du code machine à moindre frais. Par</br>contre, dans ce cadre, l'écriture de passe d'optimisations spécifiques</br>au DSL - à moins d'utiliser des techniques pointues de</br>méta-programmation - est a priori impossible.</br></br>Une seconde approche, opposée, consiste à écrire un compilateur pour</br>le DSL à partir de zéro. Toute liberté est alors donnée à</br>l'implémenteur d'intégrer à son compilateur des passes d'optimisation</br>spécifiques… mais au prix d'une réimplémentation de passes de</br>compilation déjà présentes, et certainement plus abouties, dans le</br>compilateur de son langage généraliste favori.</br></br>Dans cet exposé, je présenterai les travaux de Martin Odersky et</br>son équipe sur la virtualisation de DSLs à l'intérieur du langage de</br>programmation Scala. La virtualisation de langage utilise</br>intensivement le polymorphisme et la composition mixin de Scala ainsi</br>que des techniques de génération de code à l'exécution pour embarquer</br>des langages spécifiques dans Scala dont la compilation peut</br>réutiliser des modules du compilateur mais aussi étendre ces derniers</br>par des optimisations spécifiques au domaine. des optimisations spécifiques au domaine.)