ACM Transactions on

Computational Logic (TOCL)

Latest Articles

Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time

Choiceless Polynomial Time (CPT) is one of the most promising candidates in the search for a logic capturing Ptime. The question whether there is a... (more)

Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants

We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary... (more)

Quantitative Aspects of Linear and Affine Closed Lambda Terms

Affine λ-terms are λ-terms in which each bound variable occurs at most once, and linear λ-terms are λ-terms in which each... (more)

Compositional Synthesis of Piece-Wise Functions by Learning Classifiers

We present a novel general technique that uses classifier learning to synthesize piece-wise functions (functions that split the domain into regions... (more)

Hypersequents and Systems of Rules: Embeddings and Applications

We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting... (more)

Syntax-Preserving Belief Change Operators for Logic Programs

Recent methods have adapted the well-established AGM and belief base frameworks for belief change to cover belief revision in logic programs. In this... (more)

Modular Labelled Sequent Calculi for Abstract Separation Logics

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations.... (more)

Finite-State Map-Reduce Computation and Relational Algebra Queries

We introduce three formal models of distributed systems for query evaluation on massive databases: Distributed Streaming with Register Automata... (more)

Path Categories and Propositional Identity Types

Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky’s univalent foundations and the interpretation of Martin-Löf’s identity types in Quillen model categories as some of the highlights. In this article, we establish a connection between a natural weakening of... (more)


TOCL welcomes submissions related to all aspects of logic as it pertains to topics in computer science. The journal is published quarterly. The first issue appeared in July 2000, and the journal is indexed by ISI beginning with the 2006 volume. About

Forthcoming Articles

An Automatic Proving Approach to Parameterized Verification

Formal verification of parameterized protocols such as cache coherence protocols is a significant challenge. In this paper, we propose an automatic proving approach and its prototype paraVerifier to handle this challenge within a unified framework: (1) in order to prove the correctness of a parameterized protocol, our approach automatically discovers auxiliary invariants and the corresponding causal relations among the discovered invariants and protocol rules from a small instance of the verified protocol; (2) the discovered invariants and causal relation information are then automatically generalized into a parameterized form to construct a parameterized formal proof for a theorem prover (i.e., Isabelle). As a side product, the final verification result of a protocol is provided by a formal and human-readable proof. Our approach has been successfully applied to a number of benchmarks including snoopy-based and directory-based cache coherence protocols.

Interaction Graphs: Nondeterministic Automata

This paper exhibits a series of semantic characterisations of sublinear nondeterministic complexity classes. These results fall into the general domain of logic-based approaches to complexity theory and so-called implicit computational complexity (ICC), i.e. descriptions of complexity classes without reference to specific machine models. In particular, it relates strongly to ICC results based on linear logic since the semantic framework considered stems from work on the latter. Moreover, the obtained characterisations are of a geometric nature: each class is characterised by a specific action of a group by measure-preserving maps.

An Operational Semantics for the Cognitive Architecture ACT-R and its Translation to Constraint Handling Rules

The cognitive architecture ACT-R is popular in the field of cognitive modeling. Although it has a well-defined psychological theory, there are two problems that make it hard to reason formally about its cognitive models: First, ACT-R lacks a computational formalization of its underlying production rule system and secondly, there are many different implementations and extensions of ACT-R with many technical artifacts complicating formal reasoning even more. This paper describes a formal operational semantics -- the very abstract semantics -- that abstracts from as many technical details as possible keeping it open to extensions and different implementations of the ACT-R theory. In a second step, this semantics is refined to define some of its abstract features that are found in many implementations of ACT-R -- the abstract semantics. It concentrates on the procedural core of ACT-R and is suitable for analysis of the general transition system since it still abstracts from details like timing, the sub-symbolic layer of ACT-R or conflict resolution. Furthermore, a translation of ACT-R models to the declarative programming language CHR is defined. This makes the abstract semantics an executable specification of ACT-R. CHR has been used successfully to embed other rule-based formalisms like graph transformation systems. There are many analyis results that support formal reasoning of CHR programs. The translation of ACT-R models to CHR is proven sound and complete w.r.t. the abstract operational semantics of ACT-R. This paves the way to analysis of ACT-R models through CHR. Therefore, to the best of our knowledge, our abstract semantics is the first abstract formulation of ACT-R suitable for both analysis and execution.

Some subsystems of constant-depth Frege with parity

We consider three relatively strong families of subsystems of AC^0[2]-Frege for which exponential lower bounds on proof size are known. In order of increasing strength, these subsystems are: AC^0-Frege with parity axioms and the treelike and daglike versions of systems introduced by Krají ek which we call PK^{c}_{d}(\oplus). In a PK^{c}_{d}(\oplus)-proof, lines are cedents in which all formulas have depth at most d, parity connectives can only appear as the outermost connectives in formulas, and all but c formulas contain no parity connective at all. We give simple arguments proving that AC^0[2]-Frege is exponentially stronger than daglike PK^{O(1)}_{O(1)}(\oplus), which is exponentially stronger than treelike PK^{O(1)}_{O(1)}(\oplus). On the other hand, we point out that the best available technique for comparing the performance of such systems on De Morgan formulas, due to Impagliazzo and Segerlind, only leads to superpolynomial separations. In fact, we prove that treelike PK^{O(1)}_{O(1)}(\oplus) is quasipolynomially but not polynomially equivalent to AC^0-Frege with parity axioms. This leads us to ask the question whether any of our systems is quasipolynomially equivalent to AC^0[2]-Frege on De Morgan formulas; a positive answer would imply an exponential lower bound for AC^0[2]-Frege. We also study Itsykson and Sokolov's system Res-Lin. We prove that an extension of treelike Res-Lin is polynomially simulated by a system related to daglike PK^{O(1)}_{O(1)}(\oplus), and obtain an exponential lower bound for this system.

An Epistemic Strategy Logic

This paper presents an extension of temporal epistemic logic with operators that quantify over agent strategies. Unlike previous work on alternating temporal epistemic logic, the semantics works with systems whose states explicitly encode the strategy being used by each of the agents. This provides a natural way to express what agents would know were they to be aware of some of the strategies being used by other agents. A number of examples that rely upon the ability to express an agent's knowledge about the strategies being used by other agents are presented to motivate the framework, including reasoning about game theoretic equilibria, knowledge-based programs, and information theoretic computer security policies. Relationships to several variants of alternating temporal epistemic logic are discussed. The computational complexity of model checking the logic and several of its fragments are also characterized.

Geometry of Interaction for MALL via Hughes-vanGlabbeek Proof-Nets

This paper presents, for the first time, a Geometry of Interaction (GoI) interpretation using Hughes-vanGlabbeek (HvG) proof-nets for multiplicative additive linear logic (MALL). Our GoI captures dynamically HvGs geometric correctness criterionthe toggling cycle condition in terms of algebraic operators. Our new ingredient is a scalar extension of the *-algebra in Girard s *-ring of partial isometries over a boolean polynomial ring with literals of eigen- weights as indeterminates. In order to capture feedback arising from cuts, we construct a finer grained execution formula. The expansion of this execution formula is longer than that for collections of slices for multiplicative GoI, hence is harder to prove termination. Our GoI gives a dynamical, semantical account of boolean valuations (in particular, pruning sub-proofs), conversion of weights (in particular, ±-conversion), and additive (co)contraction, peculiar to additive proof-theory. Termination of our execution formula is shown to corre- spond to HvG s toggling criterion. The slice-wise restriction of our execution formula (by collapsing the boolean structure) yields the well known correspondence, explicit or implicit in previous works on multiplicative GoI, between the convergence of execution formulas and acyclicity of proof-nets. Feedback arising from the execution formula by restricting to the boolean polynomial structure yields autonomous definability of eigenweights among cuts from the rest of the eigenweights.

Proof Complexity Meets Algebra

We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semi-algebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence and addition of constants to a core preserve the proof complexity of the CSP. As a result, for those proof systems, the classes of constraint languages for which small unsatisfiability certificates exist can be characterised algebraically. We illustrate our results by a gap theorem saying that a constraint language either has resolution refutations of constant width, or does not have bounded-depth Frege refutations of subexponential size. The former holds exactly for the widely studied class of constraint languages of bounded width. This class is also known to coincide with the class of languages with refutations of sublinear degree in Sums-of-Squares and Polynomial Calculus over the real-field, for which we provide alternative proofs. We then ask for the existence of a natural proof system with good behaviour with respect to reductions and simultaneously small size refutations beyond bounded width. We give an example of such a proof system by showing that bounded-degree Lovász-Schrijver satisfies both requirements. Finally, building on the known lower bounds, we demonstrate the applicability of the method of reducibilities and construct new explicit hard instances of the graph 3-coloring problem for all studied proof systems.

Automated Equivalence Checking of Concurrent Quantum Processes

The novel field of quantum computation and quantum information has gathered significant momentum in the last few years. It has the potential to radically impact the future of information technology and influence the development of modern society. The construction of practical, general purpose quantum computers has been challenging, but quantum cryptographic and communication devices have been available in the commercial marketplace for several years. Quantum networks have been built in various cities around the world and a dedicated satellite has been launched by China to provide secure quantum communication. Such new technologies demand rigorous analysis and verification before they can be trusted in safety- and securitycritical applications. Experience with classical hardware and software systems has shown the difficulty of achieving robust and reliable implementations. We present a concurrent language for describing quantum systems, and develop verification techniques for checking equivalence between processes described in the language. The language has well-defined operational and superoperator semantics for protocols that are functional, in the sense of computing a deterministic input-output relation for all interleavings arising from concurrency in the system. We have implemented a tool which takes the specification and implementation of quantum protocols, described in the input language, and automatically checks their equivalence. For efficiency purposes, we restrict ourselves to Clifford operators in the stabilizer formalism, but we are able to verify protocols over all input states. We have specified and verified a collection of interesting and practical quantum protocols ranging from quantum communication and quantum cryptography to quantum error correction.

Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this paper we tackle the problems of SMT and VMT over the theories of nonlinear arithmetic over the reals (NRA) and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA). We propose a new abstraction-refinement approach for SMT and VMT on NRA or NTA, called Incremental Linearization. The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted in an abstract space limited to linear arithmetic on the rationals with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction. The method has been implemented in the MathSAT SMT solver and in the nuXmv model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach.

Minkowski Games

We introduce and study Minkowski games. These are two player games, where the players take turns to choose positions in R^d based on some rules. Variants include boundedness games, where one player wants to keep the positions bounded, and the other wants to escape to infinity; as well as safety games, where one player wants to stay within a prescribed set, while the other wants to leave it. We provide some general characterizations of which player can win such games, and explore the computational complexity of the associated decision problems. A natural representation of boundedness games yields coNP-completeness, whereas the safety games are undecidable.

A Modular Type Reconstruction Algorithm

MMT is a framework for designing and implementing formal systems in a way that systematically abstracts from theoretical and practical aspects of their type theoretical and logical foundations. Thus, definitions, theorems, and algorithms can be stated independently of the foundation, and language designers can focus on the essentials of a particular foundation and inherit a large scale implementation from MMT at low cost. Going beyond the similarly-motivated approach of meta-logical frameworks, MMT does not even commit to a particular meta-logic---that makes \mmt level results harder to obtain but also more general. We present one such result: a foundation-independent type reconstruction algorithm. It realizes the foundation-independent aspects generically relative to a set of rules that supply the foundation-specific knowledge. Maybe surprisingly, we see that the former covers most of the algorithm, including the most difficult details. Thus, we can easily instantiate our algorithm with rule sets for several important language features including, e.g., dependent function types. Moreover, our design is modular such that we obtain a type reconstruction algorithm for any combination of these features.

Automated deduction in Goedel logic

This paper addresses the deduction problem of a formula from a countable theory in the first-order G\"{o}del logic. % We generalise the well-known hyperresolution principle for deduction in G\"{o}del logic. % Our approach is based on translation of a formula to an equivalent satisfiable finite order clausal theory, consisting of order clauses. % We introduce a notion of quantified atom: a formula $a$ is a quantified atom if $a=Q x\, p(t_0,\dots,t_\tau)$ where $Q$ is a quantifier ($\forall$, $\exists$); $p(t_0,\dots,t_\tau)$ is an atom; $x$ is a variable occurring in $p(t_0,\dots,t_\tau)$; for all $i\leq \tau$, either $t_i=x$ or $x$ does not occur in $t_i$. % Then an order clause is a finite set of order literals of the form $\varepsilon_1\diamond \varepsilon_2$ where $\varepsilon_i$ is either an atom or a quantified atom, and $\diamond$ is either a connective $\geql$ or $\gle$. % $\geql$ and $\gle$ are interpreted by the equality and strict linear order on $[0,1]$, respectively. % For an input countable theory of G\"{o}del logic, the proposed translation produces a countable order clausal theory. % On the basis of the hyperresolution principle, a calculus operating over order clausal theories, is devised. % The calculus is proved to be refutation sound and complete for the countable case.

Hierarchies in Inclusion Logic with Lax Semantics

We study the expressive power of fragments of inclusion logic under the so-called lax team semantics. The fragments are defined either by restricting the number of universal quantifiers, the number of inclusion atoms, or the arity of inclusion atoms. We show that the whole expressive power of inclusion logic can be captured using only five inclusion atoms in finite ordered models, or alternatively only one universal quantifier in general. The arity hierarchy is shown to be strict by relating the question to the study of arity hierarchies in fixed point logics.

Relating paths in transition systems: the fall of the modal mu-calculus

We revisit Janin and Walukiewiczs classic result on the expressive completeness of the modal mu-calculus with respect to Monadic Second Order Logic (MSO), which is that the mu-calculus corresponds precisely to the fragment of MSO that is invariant under bisimulation. We show that adding binary relations over finite paths in the picture may alter the situation. We consider a general setting where finite paths of transition systems are linked by means of a fixed binary relation. This setting gives rise to natural extensions of MSO and the mu-calculus, that we call the MSO with paths relation and the jumping mu-calculus, the expressivities of which we aim at comparing. We first show that bounded-memory binary relations bring about no additional expressivity to either of the two logics, and thus preserve expressive completeness. In contrast, we show that for a natural, classic infinite-memory binary relation stemming from games with imperfect information, the existence of a winning strategy in such games, though expressible in the bisimulation-invariant fragment of MSO with paths relation, cannot be expressed in the jumping mu-calculus. Expressive completeness thus fails for this relation. These results crucially rely on our observation that the jumping mu-calculus has a tree automata counterpart: the jumping tree automata. We also prove that for observable winning conditions, the existence of winning strategies in games with imperfect information is expressible in the jumping mu-calculus. Finally, we derive from our main theorem that jumping automata cannot be projected, and ATL with imperfect information does not admit expansion laws.


Publication Years 2000-2018
Publication Count 506
Citation Count 5079
Available for Download 506
Downloads (6 weeks) 643
Downloads (12 Months) 6983
Downloads (cumulative) 146771
Average downloads per article 290
Average citations per article 10
First Name Last Name Award
Foto Afrati ACM Fellows (2014)
Noga Alon ACM Fellows (2016)
Rajeev Alur ACM Fellows (2007)
Robert Brayton ACM Paris Kanellakis Theory and Practice Award (2006)
Randal E Bryant ACM Fellows (2000)
ACM Paris Kanellakis Theory and Practice Award (1998)
Peter Buneman ACM Fellows (2000)
Stephen A Cook ACM Fellows (2008)
ACM A. M. Turing Award (1982)
Thierry Coquand ACM Software System Award (2013)
Giuseppe De Giacomo ACM Fellows (2015)
Wenfei Fan ACM Fellows (2012)
Georg Gottlob ACM Fellows (2007)
Martin Grohe ACM Fellows (2017)
Orna Grumberg ACM Fellows (2015)
Yuri Gurevich ACM Fellows (1997)
Joseph Halpern ACM AAAI Allen Newell Award (2008)
ACM Fellows (2002)
Robert Harper ACM Fellows (2005)
Thomas A Henzinger ACM Fellows (2006)
Vasant Honavar ACM Senior Member (2006)
Neil Immerman ACM Fellows (2002)
Neil Jones ACM Fellows (1998)
Daphne Koller ACM Prize in Computing (2007)
Dexter Kozen ACM Fellows (2003)
Sarit Kraus ACM Fellows (2014)
K. Rustan M. Leino ACM Fellows (2016)
Maurizio Lenzerini ACM Fellows (2009)
Leonid Libkin ACM Fellows (2012)
Tova Milo ACM Fellows (2012)
Lawrence C Paulson ACM Fellows (2008)
Frank Pfenning ACM Fellows (2015)
ACM Senior Member (2007)
Andre Platzer ACM Senior Member (2017)
ACM Doctoral Dissertation Award
Honorable Mention (2009)
Raymond Reiter ACM Fellows (1997)
Thomas Reps ACM Fellows (2005)
ACM Doctoral Dissertation Award (1983)
Mooly Sagiv ACM Fellows (2015)
Peter James Stuckey ACM Distinguished Member (2009)
Dan Suciu ACM Fellows (2011)
Moshe Y Vardi ACM Presidential Award (2017)
Outstanding Contribution to ACM Award (2009)
ACM Presidential Award (2008)
ACM Paris Kanellakis Theory and Practice Award (2005)
ACM Fellows (2000)
Victor Vianu ACM Fellows (2006)
Philip Wadler ACM Fellows (2007)
Reinhard Wilhelm ACM Distinguished Service Award (2010)
ACM Fellows (2000)
Pierre Wolper ACM Paris Kanellakis Theory and Practice Award (2005)
Michael Wooldridge ACM Fellows (2015)
Qiang Yang ACM Fellows (2017)
ACM Distinguished Member (2011)
Mihalis Yannakakis ACM Fellows (1998)
Ron van der Meyden ACM Distinguished Member (2009)

First Name Last Name Paper Counts
Yuri Gurevich 10
Andreas Blass 8
Thomas Eiter 8
Orna Kupferman 8
Thomas Henzinger 7
Frank Neven 6
VS Subrahmanian 6
Michael Zakharyaschev 5
Michael Benedikt 5
Ranko Lazić 5
Nicola Olivetti 5
Massimo Lauria 5
Georg Gottlob 5
Marc Denecker 5
Krishnendu Chatterjee 5
Paolo Liberatore 5
Hans Tompits 4
Thomas Schwentick 4
Luc Segoufin 4
Leonid Libkin 4
Nadia Creignou 4
Georg Struth 4
Heribert Vollmer 4
Stefan Woltran 4
Alessio Guglielmi 4
Erich Grädel 3
Arnold Beckmann 3
Joost Vennekens 3
Fabio Mogavero 3
Aniello Murano 3
Guido Fiorino 3
Andrzej Murawski 3
Yidong Shen 3
Emanuel Kieroński 3
Juha Kontinen 3
Mauro Ferrari 3
Camillo Fiorentini 3
Paulo Shakarian 3
Grigoris Antoniou 3
Randal Bryant 3
Neil Thapen 3
Krzysztof Apt 3
Stefan Szeider 3
Frank Pfenning 3
Olivier Serre 3
Samuel Buss 3
Manuel Bodirsky 3
Olaf Beyersdorff 3
Joseph Halpern 3
Maurizio Gabbrielli 3
Fangzhen Lin 3
Silvio Ghilardi 3
Stéphane Demri 3
Jürgen Dix 3
Dale Miller 3
Yuan Feng 3
Moshe Vardi 3
Jakob Nordström 3
Dexter Kozen 3
Maria Meo 3
Alwen Tiu 3
Chiaki Sakama 3
Rajeev Alur 3
Agata Ciabattoni 3
Gerardo Simari 3
Samir Genaim 3
Véronique Cortier 3
Tony Tan 3
Albert Atserias 3
Jiahuai You 3
Ke Wang 3
Thomas Lukasiewicz 3
Nicola Galesi 3
Simone Martini 2
Filippo Bonchi 2
Eugénie Foustoucos 2
Stephen Cook 2
Mariangiola Dezani-Ciancaglini 2
Camilla Schwind 2
Frank Stephan 2
Daniele Nardi 2
David Billington 2
Guido Governatori 2
Michael Maher 2
Pierre Wolper 2
Felix Klaedtke 2
Jakob Simonsen 2
Kristina Sojakova 2
Ori Lahav 2
Stefan Rümmele 2
Nachum Dershowitz 2
Hana Chockler 2
Agostino Dovier 2
Francesco Ranzato 2
Hubie Chen 2
Klaus Aehlig 2
Helmut Veith 2
Wouter Gelade 2
Kousha Etessami 2
Arnaud Carayol 2
Uwe Egly 2
Roman Kontchakov 2
Andreas Krebs 2
Maciej Komosinski 2
Michael Fisher 2
Giorgi Japaridze 2
Robert Nieuwenhuis 2
Mirosław Truszczyński 2
Andrea Asperti 2
Carsten Lutz 2
Vladislav Ryzhikov 2
Cristian Molinaro 2
Michael Elberfeld 2
Simone Bova 2
Adam Kups 2
John Derrick 2
Arie Gurfinkel 2
Witold Charatonik 2
Torsten Schaub 2
Silvia Crafa 2
Valentin Goranko 2
Marcello Bonsangue 2
Alexandra Silva 2
Nicola Leone 2
Axel Polleres 2
Wolfgang Faber 2
Rakesh Verma 2
Gian Pozzato 2
Panos Rondogiannis 2
Arnaud Durand 2
Paqui Lucio 2
Barnaby Martin 2
Jan Otop 2
Renate Schmidt 2
Michael Kaminski 2
Stefan Ratschan 2
Robert Harper 2
Venkatramanan Subrahmanian 2
Frank Wolter 2
Laura Giordano 2
Scott Weinstein 2
Nicole Schweikardt 2
Alexander Artikis 2
Marek Sergot 2
Maria Bonacina 2
Arne Meier 2
Ugo Montanari 2
Rohit Chadha 2
Axel Haddad 2
Orna Grumberg 2
Luigi Palopoli 2
Diego Calvanese 2
James Worrell 2
Giovambattista Ianni 2
Guillem Godoy 2
Victor Vianu 2
Ullrich Hustadt 2
Stavros Cosmadakis 2
Martin Grohe 2
Trancao Son 2
Laurent Doyen 2
Andrei Voronkov 2
William Wadge 2
Francesca Rossi 2
Roberto Sebastiani 2
Jónathan Heras 2
Florian Rabe 2
Fabrizio Angiulli 2
Damiano Zanardini 2
Maurice Bruynooghe 2
Brigitte Pientka 2
Elvira Albert 2
Jeremy Avigad 2
ROB Van Glabbeek 2
Jeffery Zucker 2
Udi Boker 2
Ilka Schnoor 2
Vladimir Lifschitz 2
Pascal Van Hentenryck 2
Churnjung Liau 2
Jean Raskin 2
Clare Dixon 2
Silvio Ranise 2
Ralf Küsters 2
Paul Gastin 2
Mingsheng Ying 2
Lawrence Paulson 2
Karl Crary 2
Valentina Gliozzi 2
Marco Cadoli 2
Michael Fink 2
Wan Fokkink 2
Riccardo Rosati 2
Jean Marion 2
Stefano Bistarelli 2
Olivier Danvy 2
Morgan Deters 2
Hitoshi Furusawa 2
Salvatore La Torre 2
Stefan Szeider 2
André Platzer 2
John Tucker 2
Stefan Göller 2
Ugo Lago 2
Jeroen Keiren 2
Henning Schnoor 2
Miroslav Velev 2
Stéphanie Delaune 2
Gerald Pfeifer 2
Anuj Dawar 2
Mantas Šimkus 2
Dirk Vermeir 2
Michaël Rusinowitch 2
David Gilis 2
Richard Trefler 2
Amy Sliva 2
Agi Kurucz 2
Lutz Schröder 2
Robert Ganian 1
Mikołaj Bojańczyk 1
Claire David 1
Jérôme Lang 1
Christoph Weidenbach 1
Ştefan Ciobâcă 1
Rastislav Lenhardt 1
John Dickerson 1
Joël Ouaknine 1
Lara Spendier 1
Patrik Simons 1
Deborah East 1
Oleg Verbitsky 1
Marijn Heule 1
Peter Schneider-Kamp 1
Ursula Martin 1
Paulo Oliva 1
Thomas Schneider 1
Michele Bugliesi 1
Steven German 1
Salvatore Ruggieri 1
Holger Sturm 1
Arun Sharma 1
Pawel Mielniczuk 1
Marco Bernardo 1
Manuel Clavel 1
Sabina Rossi 1
Ara Hayrapetyan 1
James Bailey 1
Guozhu Dong 1
Helmut Seidl 1
Akitoshi Kawamura 1
Konstantin Korovin 1
Parthasarathy Madhusudan 1
Frédéric Servais 1
Jeremy Pitt 1
Carmen Gervet 1
Alessandro Armando 1
Sebastian Danicic 1
Mihalis Yannakakis 1
Floris Geerts 1
Enrica Nicolini 1
Katsumi Inoue 1
Sophie Laplante 1
Roy Dyckhoff 1
Isabella Mastroeni 1
Alan Schmitt 1
Georgios Paliouras 1
Eryk Kopczyński 1
Raymond Reiter 1
Sebastian SardiñA 1
Sasha Rubin 1
César Domínguez 1
Julio Rubio 1
Michael Blondin 1
Matthew Stone 1
Jia Tao 1
Irina Trubitsyna 1
Aleksandar Nanevski 1
Liliana Pasquale 1
Ruggero Lanotte 1
Cynthia Kop 1
Heng Zhang 1
Francesco Scarcello 1
Mohua Banerjee 1
Anca Muscholl 1
Nir Friedman 1
Martin Grohe 1
Piotr Witkowski 1
Filip Mazowiecki 1
Terrance Swift 1
Nathalie Sznajder 1
Revantha Ramanayake 1
Włodzimierz Drabent 1
Diogo Henriques 1
Tomi Janhunen 1
Michael Warren 1
Christopher Hampson 1
Amelie David 1
Alban Ponse 1
Jürgen Giesl 1
Itay Neeman 1
Michael Bauland 1
Anastasia Analyti 1
Howard Bowman 1
Peter Buneman 1
Pavlos Peppas 1
Konstantinos Chatzikokolakis 1
Emmanuel Polonowski 1
Slim Abdennadher 1
Francesca Scozzari 1
Yi Zhou 1
Zhaohui Luo 1
Kumar Verma 1
Bruce Kapron 1
Ngoc Nguyen 1
Benedikt Bollig 1
Sheila McIlraith 1
John Hitchcock 1
Sara Cohen 1
Bjørn Kjos-Hanssen 1
Sara More 1
Pavel Naumov 1
Svenja Schalthöfer 1
Erkal Selman 1
Shambwaditya Saha 1
Zhé Hóu 1
Bas Luttik 1
Marco Gaboardi 1
Carlo Furia 1
Reinhard Pichler 1
Sofie Haesevoets 1
Eugenia Ternovska 1
Daniele Zucchelli 1
Taolue Chen 1
Alexandru Mereacre 1
Arnon, Avron 1
Yuval Filmus 1
Daniel Schwartz 1
Gianluigi Greco 1
Agustín Valverde 1
David Pearce 1
Fariba Sadri 1
Bakhadyr Khoussainov 1
Markus Aschinger 1
María Poza 1
Serge Haddad 1
Davide Bresolin 1
Charles Paperman 1
Antonino Salibra 1
Harald Zankl 1
Prahladh Harsha 1
Gabriel Ebner 1
Carla Piazza 1
Frank De Boer 1
Dorota Leszczyńska-Jasion 1
Paola Spoletini 1
Nicholas Radcliffe 1
Dirk Pattinson 1
Paola Bruscoli 1
Naoki Nishida 1
Cheping Su 1
Enrique Martin-Martin 1
Michael Boom 1
Andrei Bulatov 1
Lutz Burger 1
Manfred Schmidt-Schauß 1
Andreas Herzig 1
Kumud Sanwal 1
Sebastian Müller 1
Ulrich Schöpp 1
Matthias Horbach 1
Joost Engelfriet 1
Mirco Nanni 1
Ron Van Der Meyden 1
Steve Kremer 1
Bart Bogaerts 1
Ian Hayes 1
Markus Lohrey 1
Jia Tao 1
Anatoli Degtyarev 1
Sarit Kraus 1
Lutz Straßburger 1
Massimo Benerecetti 1
Flemming Nielson 1
Hanne Nielson 1
Dmitry Shkatov 1
Jeroen Janssen 1
Prakash Panangaden 1
Ofer Arieli 1
Fred Mesnard 1
Oliver Kutz 1
Greta Yorsh 1
Alexander Rabinovich 1
Jean Moyen 1
Naohi Eguchi 1
Pierre Valarcher 1
Neil Jones 1
Paolo Coppola 1
Thom Frühwirth 1
Xiaoping Chen 1
Daniel Stamate 1
José Meseguer 1
Chitta Baral 1
Evelina Lamma 1
Colin Hirsch 1
Vincent Danos 1
Philip Wadler 1
Raymond Mcdowell 1
Luca Roversi 1
Pavol Černý 1
Lidia Tendera 1
Sebastian Binnewies 1
Rajeev Goré 1
Luca Aceto 1
Ugo de’Liguoro 1
Mateu Villaret 1
Matteo Rossi 1
Axel Legay 1
Alessandro Cimatti 1
Alberto Griggio 1
Bart Kuijpers 1
Véronique Bruyère 1
Bas Ketsman 1
Daniel Zinn 1
Petar Marković 1
Nils Gesbert 1
Maciej Gazda 1
Sharon Shoham 1
Michele Loreti 1
Yangjia Li 1
Iyad Kanj 1
Trung Van Pham 1
Christopher Porter 1
Nathanaël Fijalkow 1
Noga Alon 1
Bernard Boigelot 1
Steffen Van Bakel 1
Leroy Chew 1
Chih Ong 1
Andrea Tubella 1
Thomas Wilke 1
Frederik Harwath 1
Frédéric Benhamou 1
David Griffioen 1
Frits Vaandrager 1
Giuseppe Perelli 1
Samir Genaim 1
Stefano Guerrini 1
Yan Zhang 1
Denis Ponomaryov 1
Mikhail Soutchanski 1
Pablo Muñoz 1
Szymon Chlebowski 1
David Baelde 1
Cinzia Di Giusto 1
Clemens Ley 1
Konstantinos Mamouras 1
Luca Alfaro 1
Pierre Marquis 1
Adnan Aziz 1
Roberto Cosmo 1
Martin Hofmann 1
Hendrik Hoogeboom 1
Alessio Lomuscio 1
Michał Skrzypczak 1
Martin Gebser 1
Mnacho Echenim 1
José Alferes 1
P Mateus 1
Vasant Honavar 1
Christoph Berkholz 1
Bettina Fazzinga 1
K Leino 1
Sebastian Nanz 1
Roman Schindlauer 1
Carlos Damásio 1
Qiang Yang 1
Diego Figueira 1
Costas Koutras 1
Linh Nguyen 1
Mario Bravetti 1
Roberto Gorrieri 1
David McAllester 1
Ashish Tiwari 1
Christophe Rigotti 1
Stephan Kreutzer 1
Laurent Michel 1
Matthew Bauer 1
Roberto Bruttomesso 1
Diego Recupero 1
Jack Lutz 1
Russell Harmer 1
Jules Desharnais 1
Nam Tran 1
Sebastiaan Terwijn 1
Furio Honsell 1
Toni Mancini 1
Jan Johannsen 1
Marcel Marquardt 1
Daniel Neider 1
Pierre Lescanne 1
Francesco Genco 1
Tony Tan 1
Michael Laurence 1
Venkatramanan Subrahmanian 1
Francesco Santini 1
Fang Wei 1
Edward Hung 1
Chiuwo Choi 1
Jose Gaintzarain 1
Julien Truffaut 1
Silvia Tomasi 1
Bertram Felgenhauer 1
Martin Lange 1
Nathalie Bertrand 1
Ronald De Haan 1
George Barmpalias 1
Douglas Cenzer 1
Guido Sciavicco 1
Dan Suciu 1
Miika Hannula 1
Fabrizio Riguzzi 1
Mariusz Urbański 1
Fabio Gadducci 1
Heike Wehrheim 1
Benno Van Den Berg 1
Richard Garner 1
Nils Klarlund 1
Vigyan Singhal 1
Vincent Cheval 1
Till Tantau 1
Ian Pratt-Hartmann 1
Matthias Knorr 1
Jeanchristoph Jung 1
Shulamit Halamish 1
Gaëlle Fontaine 1
Rémy Chrétien 1
Francesco Donini 1
Piero Bonatti 1
Sylvain Schmitz 1
Johannes Fichte 1
Luís Pinto 1
Ferruccio Guidi 1
Rob Arthan 1
Christian Urban 1
James Cheney 1
Austin Parker 1
Wenfei Fan 1
Ewa Madalińska-Bugaj 1
Danny De Schreye 1
Francesco Quaglia 1
Rachel Ben-Eliyahu -- Zohary 1
Nobuyuki Suzuki 1
Doron Peled 1
Toshiyasu Arai 1
Richard Mckinley 1
Stefan Milius 1
Sandro Etalle 1
David Fernández-Duque 1
Robin Adams 1
Yannick Chevalier 1
Mathieu Turuani 1
Paola Mello 1
Paolo Torroni 1
Vernon Asuncion 1
Enrico Pontelli 1
Krishnendu Chatterjee 1
Cindy Eisner 1
Dana Fisman 1
Paliath Narendran 1
David Pym 1
Lucas Bordeaux 1
Lizhu Zhou 1
Giuliana Sabbatini 1
Murdoch Gabbay 1
Marcel Jackson 1
Wied Pakusa 1
Ranald Clouston 1
Benno Berg 1
Lou Dries 1
Jordi Levy 1
Mahesh Viswanathan 1
Vincent Siles 1
Lise Getoor 1
Etienne Grandjean 1
Thierry Coquand 1
Jeroen Ketema 1
H Macpherson 1
Mehrnoosh Sadrzadeh 1
Davide Sangiorgi 1
Kensuke Kojima 1
Martin Luck 1
Albert Rubio 1
Pierre Genevès 1
Anastasios Skarlatidis 1
Sjoerd Cranen 1
Mladen Mikša 1
Marc Vinyals 1
Ph Schnoebelen 1
Christel Baier 1
Hector Levesque 1
Dominic Hughes 1
Rocco De Nicola 1
Bard Bloom 1
Mingsheng Ying 1
Nengkun Yu 1
Johannes Schmidt 1
Alessandro Artale 1
Jerzy Tiuryn 1
Sébastien Jodogne 1
Meena Mahajan 1
Vincent Van Oostrom 1
Elliot Fairweather 1
Eli Ben-Sasson 1
Marco Calautti 1
Howard Straubing 1
Franco Montagna 1
Marc Christie 1
Anthonywidjaja Lin 1
Isabelle Gnaedig 1
Hélène Kirchner 1
Pablo Barceló 1
Przemysław Daca 1
Jan Křetínský 1
Tim Willemse 1
Balder Cate 1
Mdaquil Khan 1
Floor Sietsma 1
M Praveen 1
Abu Masud 1
Angelos Charalambidis 1
Makoto Tatsuta 1
Alexis Saurin 1
Jean Puget 1
Laurent Perron 1
Mark Ryan 1
Alessandro Facchini 1
Lorenzo Carlucci 1
Daria Walukiewicz-Chrząszcz 1
Brijesh Dongol 1
Lian Wen 1
Giora Slutzki 1
Boris Konev 1
Francesco Parisi 1
Jos De Bruijn 1
Alexander Serebrenik 1
Florian Horn 1
Martin Mundhenk 1
Samuel Shen 1
Jeremy Bryans 1
Sophia Knight 1
Viviana Bono 1
Robert Givan 1
Marco Pedicini 1
Thomas Reps 1
Tristan Crolard 1
Paweł Urzyczyn: 1
Aleksy Schubert 1
Andrea Formisano 1
Nathan Segerlind 1
Mathieu Baudet 1
Aleksandar Ignjatović 1
Nicolas Spyratos 1
David Basin 1
Rupak Majumdar 1
Hubert Comon-Lundh 1
Octavian Udrea 1
Marco Gavanelli 1
Martin Otto 1
Marc Zeitoun 1
Pavel Pudlák 1
Bernhard Möller 1
Michael Mendler 1
Viorica Sofronie-Stokkermans 1
James Harland 1
Fabio Alessi 1
Kazuhisa Makino 1
Alessandro Bianco 1
Zhiqiang Zhuang 1
Kewen Wang 1
Yiannis Moschovakis 1
Luca Iocchi 1
Stephan Schulz 1
Stefano Berardi 1
Robert Hierons 1
Michael Thomas 1
Richard Lassaigne 1
Jimmy Lee 1
Wojciech Kazana 1
Marco Diciolla 1
Anders Mörtberg 1
Adrian Haret 1
Petar Dapić 1
Irena Schindler 1
Jean Jouannaud 1
Nabil Layaïda 1
Simon Kramer 1
Wieger Wesselink 1
Tim Willemse 1
Enrico Marchioni 1
Zhe Wang 1
Rodney Topor 1
David Gray 1
Kevin Donnelly 1
Fabio Massacci 1
Alain Finkel 1
Christoph Haase 1
George Metcalfe 1
Dov Gabbay 1
Anil Shukla 1
Matthew Hague 1
Yde Venema 1
Marko Samer 1
Pavel Naumov 1
Sergio Greco 1
Eric Languénou 1
Frédéric Goualard 1
Terrance Swift 1
Jan Groote 1
Gerhard Schellhorn 1
Simone Tini 1
Andrea Masini 1
Carsten Fuhs 1
Tuanfang Fan 1
Phuong Nguyen 1
Michel Reniers 1
Yan Zhang 1
C Ong 1
Arthur Charlesworth 1
Adrià Gascón 1
Konstantinos Handjopoulos 1
Johan Wittocx 1
Robert Brayton 1
Elio Giovannetti 1
Saguy Benaim 1
Nicolas Peltier 1
Yavor Nenov 1
James Delgrande 1
Alexander Kartzow 1
Adam Trybus 1
Ilkka Niemelä 1
Dietmar Seipel 1
Novak Novaković 1
Peter Lumsdaine 1
Jakub Michaliszyn 1
Joséespírito Santo 1
Marcin Jurdziński 1
Stefan Berghofer 1
Liyan Yuan 1
Mary Williams 1
Catuscia Palamidessi 1
Guy Rey 1
Sofie Verbaeten 1
Doron Bustan 1
Marco Schaerf 1
Mooly Sagiv 1
Reinhard Wilhelm 1
Alexander Razborov 1
Eugenio Omodeo 1
Markus KröTzsch 1
Sebastian Rudolph 1
Dominique Larchey-Wendling 1
Didier Galmiche 1
Dmitry Tishkovsky 1
Jan Smaus 1
Roberto Giacobazzi 1
Lan Zhang 1
Prakash Panangaden 1
Jan Rutten 1
Anthonywidjaja To 1
Eugen Zălinescu 1
Federico Chesani 1
Yan Zhang 1
Yuxin Deng 1
Christopher Stone 1
Peter Thiemann 1
Werner Nutt 1
Gerald Lüttgen 1
Gilles Dowek 1
Hirotaka Ono 1
Jason Teutsch 1
Franz Baader 1
Bela Stantic 1
Anna Ingólfsdóttir 1
Simona Ronchi Della Rocca 1
Sławomir Lasota 1
Sylvain Peyronnet 1
Frédéric Magniez 1
Michel De Rougemont 1
Johan Thapper 1
Atsushi Igarashi 1
George Vouros 1
Christian Sattler 1
Oliver Friedmann 1
Małgorzata Biernacka 1
Shuvendu Lahiri 1
Jan Bussche 1
Conrad Drescher 1
Robert Simmons 1
Tova Milo 1
Neil Immerman 1
Iddo Tzameret 1
Sebastian Eberhard 1
Stefan Hetzl 1
Kord Eickmeyer 1
Shqiponja Ahmetaj 1
Susmit Sarkar 1
Gianfranco Rossi 1
Florent Madelaine 1
Giuseppe Giacomo 1
Luis Moraes 1
Marsha Chećhik 1
Antonio Flores-Montoya 1
Simona Perri 1
Paolo Ferraris 1
Ernie Cohen 1
Daphne Koller 1
Filip Murlak 1
Matthias Broecheler 1
Odile Papini 1
Anna Zamansky 1
M Biscaia 1
Guy Avni 1
Sergio Flesca 1
Serenella Cerrito 1
Jan Bergstra 1
René Thiemann 1
Erik Mathiesen 1
Alberto Momigliano 1
Steven Schockaert 1
Martin Peim 1
Konstantinos Sagonas 1
Annabelle McIver 1
Carroll Morgan 1
Romain Péchoux 1
Lars Kristiansen 1
Russell Impagliazzo 1
Pascal Hitzler 1
Hariolf Betz 1
Jianmin Ji 1
K Subramani 1
Yann Loyer 1
Annalisa Bossi 1
Wim Hesselink 1
Helle Hansen 1
Anastasios Sidiropoulos 1
Stijn Heymans 1
Davy Van Nieuwenborgh 1
Marco Alberti 1
Helmut Schwichtenberg 1
Benjamin Monmege 1
John Havlicek 1
Hubert Comon 1
Zbigniew Lonc 1
Stavros Tripakis 1
Runyao Duan 1
Zhengfeng Ji 1
Adel Bouhoula 1
Yehoshua Sagiv 1
Robert Goldblatt 1
Neil Yorke-Smith 1
Igor Walukiewicz 1
Emmanuel Dall'olio 1
Peter Stuckey 1
Marta Kwiatkowska 1
Ian Zerny 1
Tom Ameloot 1
Aart Middeldorp 1
Nicolai Kraus 1
Michael Wooldridge 1
Paul Raff 1
Stijn Vansummeren 1
Giuseppe De Giacomo 1
Luigia Aiello 1
Nada Lavrač 1
Peter Flach 1
Victor Marek 1
Antonis Kakas 1
James Lynch 1
Teodor Przymusinski 1
Stefan Brass 1
Peter Jonsson 1
Emilio Muñoz-Velasco 1
Micah Adler 1
Foto Afrati 1
Jonni Virtema 1
Maribel Fernández 1
Jan Kára 1
Kedar Namjoshi 1
Detlef Kähler 1
Moritz Müller 1
Magdalena Ortiz 1
Andy King 1
Maurizio Lenzerini 1
Giacoma Monreale 1
Achille Frigeri 1
David Jansen 1
Anton Wijs 1
Tatjana Petrov 1
Naghmeh Ghafari 1

Affiliation Paper Counts
University of Missouri System 1
CSIRO Data61 1
University of Tokyo 1
University of Hawaii at Manoa 1
West Virginia University 1
Goethe University Frankfurt 1
Boston College 1
University of Leipzig 1
Universite de Versailles Saint-Quentin-en-Yvelines 1
University of Mons-Hainaut 1
Shanghai Jiaotong University 1
LogicBlox Inc 1
Harvey Mudd College 1
Institute of Informatics and Telecommunications, Athens 1
Institute for Work and Health (IST) 1
RMIT University 1
Warsaw University of Technology 1
BRICS Basic Research in Computer Science 1
University of California, Los Angeles 1
Friedrich Schiller University Jena 1
Institute of Computer Science Crete 1
University of Oslo 1
University of Sussex 1
University of Wurzburg 1
Bar-Ilan University 1
University of California, Santa Cruz 1
Freescale Semiconductor 1
Telcordia Technologies, Inc. 1
University of Wyoming 1
Yale NUS College 1
Open University of the Netherlands 1
University of California, Riverside 1
Martin Luther University of Halle-Wittenberg 1
Northeastern University 1
INRIA Rhone-Alpes 1
University of Richmond 1
Vietnamese Academy of Science and Technology 1
Kyushu University 1
Tokyo Institute of Technology 1
University of Washington, Seattle 1
Universite de La Reunion 1
Charles University 1
Polytechnic Institute of Bari 1
University of Urbino 1
Philipps-Universitat Marburg 1
University of California System 1
Texas State University-San Marcos 1
NEC Deutschland GmbH 1
National Institute of Advanced Industrial Science and Technology 1
Medical University of Innsbruck 1
Avaya Inc. 1
Laboratoire d'Informatique Fondamentale de Marseille 1
Microsoft Research Cambridge 1
University of Bristol 1
INRIA Rocquencourt 1
Clarkson University 1
Kalamazoo College 1
Tianjin University 1
National Penghu University 1
Alexandru Ioan Cuza University 1
University of Heidelberg 1
Vassar College 1
Demokritos National Centre for Scientific Research 1
University of Genoa 1
Vinh University 1
Capital University of Economics and Business China 1
State University of New York at Albany 1
Faculdade de Ciencias e Tecnologia, New University of Lisbon 1
Lero - The Irish Software Engineering Research Centre 1
Cardiff University 1
University of Birmingham 1
Technische Universitat Braunschweig 1
Georgia Institute of Technology 1
Uppsala University 1
University of Perugia 1
DePaul University 1
University of Queensland 1
German University in Cairo 1
Istituto Per Le Applicazioni Del Calcolo Mauro Picone, Rome 1
Universitat de Girona 1
Munich University of the Federal Armed Forces 1
University of Seville 1
Nokia Corporation 1
Massachusetts Institute of Technology 1
University of Carthage 1
University of Witwatersrand 1
Swiss Federal Institute of Technology, Lausanne 1
University of Bern 1
Grenoble INP ENSIMAG 1
Universite Pierre et Marie Curie 1
Institute of Computer Science of the Polish Academy of Sciences 1
University of Konstanz 1
Karlsruhe Institute of Technology 1
Saarland University 1
Harvard University 1
University of Parma 1
Universite de Lorraine 1
Universite Paris-Sud XI 1
Laboratoire d'Analyse et Modelisation de Systemes pour l'Aide a la Decision 1
Universite d'Artois 1
Universite de Bordeaux 1
Kassel University 1
National University of Ireland, Galway 1
Boston University 1
University of Peloponnese 1
University of Florida 1
United States Military Academy 1
Victoria University of Wellington 1
La Trobe University 1
National Technical University of Athens 1
SRI International 1
Academic College of Tel-Aviv - Yaffo 1
University of Vienna 1
Bryn Mawr College 1
University of Wisconsin Madison 1
Hong Kong Polytechnic University 1
Vrije Universiteit Amsterdam 1
University of St Andrews 1
Laval University 1
Florida State University 1
INRIA Lorraine 1
University of Bonn 1
University of Paderborn 1
The Interdisciplinary Center Herzliya 1
Queensland University of Technology 1
Purdue University 1
Drake University 1
National Taiwan University 1
University of Erlangen-Nuremberg 1
Lafayette College 1
University of Twente 1
University of Illinois 1
CSIC - Instituto de Investigacion en Inteligencia Artificial 1
Columbia University 1
Weizmann Institute of Science Israel 1
Stockholm University 1
Johannes Gutenberg University Mainz 1
Athens University of Economics and Business 1
IBM Haifa Labs 1
University of Southern Denmark 1
Jozef Stefan Institute 1
European Commission 1
AT&T Laboratories Florham Park 1
University of Minnesota System 1
University of Opole 1
Ben-Gurion University of the Negev 1
National University Corporation Shizuoka University 1
Tata Institute of Fundamental Research 1
Laboratoire Bordelais de Recherche en Informatique 1
Universite de Caen Normandie 1
University of Groningen 1
University of Haifa 1
University of Stirling 1
Novosibirsk State University 1
Ryerson University 1
Nagoya University 1
University of Trier 2
IRIT Institut de Recherche Informatique de Toulouse 2
University of Victoria 2
Kobe University 2
Beijing University of Technology 2
Universite Paris-Est 2
Google Inc. 2
University of Durham 2
New York University 2
Heriot-Watt University, Edinburgh 2
Rutgers, The State University of New Jersey 2
Informatique, Biologie Integrative et Systemes Complexes 2
University of Eastern Piedmont Amedeo Avogadro, Alessandria 2
Technical University of Clausthal 2
University of Dundee 2
Linkoping University 2
Fondazione Bruno Kessler 2
University of Tubingen 2
Chinese University of Hong Kong 2
Jacobs University Bremen 2
Institute of Software Chinese Academy of Sciences 2
Universidad de Malaga 2
INRIA Institut National de Rechereche en Informatique et en Automatique 2
McDaniel College 2
The University of Sydney 2
University of Massachusetts Amherst 2
Iowa State University 2
IBM Research 2
University of Melbourne 2
University of Augsburg 2
Arizona State University 2
University of L'Aquila 2
University of Ulm 2
Universite de Lyon 2
Utrecht University 2
University of Nottingham 2
Ecole Normale Superieure de Cachan 2
Ecole des Mines de Nancy 2
University of Auckland 2
University of Science and Technology of China 2
University of Florence 2
Macquarie University 2
Brunel University London 2
McMaster University 2
Research Organization of Information and Systems National Institute of Informatics 2
Indian Institute of Technology, Kanpur 2
Universidad del Pais Vasco - Euskal Herriko Unibertsitatea, Campus Bizkaia 2
Kyoto University 2
Institute for Advanced Studies 2
IBM Thomas J. Watson Research Center 2
University of Crete 2
University of London 2
Aalto University 2
Ecole Normale Superieure de Lyon 2
Poznan University of Technology 2
Manchester Metropolitan University 2
Kagoshima University 2
Reykjavik University 2
University of the Basque Country 2
University of Novi Sad 2
University of Minho 2
Wright State University 2
Politecnico di Milano 2
National University of Singapore 2
CNRS Centre National de la Recherche Scientifique 2
Leiden University 3
University of Piraeus 3
Technical University of Dresden 3
Royal Holloway University of London 3
University of Potsdam 3
TU Dortmund University 3
University of Milan - Bicocca 3
Rice University 3
Institute of Mathematical Sciences India 3
Technical University of Denmark 3
University of Technology Sydney 3
Universite Paul Cezanne Aix-Marseille III 3
Universidad de Chile 3
Wakayama University 3
University of Leeds 3
Chinese Academy of Sciences 3
Villanova University 3
University of Siena 3
University of Kentucky 3
Chalmers University of Technology 3
University of Waterloo 3
Universidad de La Rioja 3
Universite Libre de Bruxelles 3
New Mexico State University Las Cruces 3
Pennsylvania State University 3
Lubeck University 3
Laboratoire d'Informatique de l'Ecole Polytechnique 3
University of Patras 3
Brown University 3
Academia Sinica Taiwan 3
Australian National University 3
Universidade de Lisboa 3
Universite Henri Poincare 3
INRIA Saclay 3
Hong Kong University of Science and Technology 3
Laboratoire de Recherche en Informatique 4
University of Innsbruck 4
Center for Mathematics and Computer Science - Amsterdam 4
Laboratoire d'Informatique de Nantes-Atlantique 4
University of G. d'Annunzio Chieti and Pescara 4
LORIA Laboratoire Lorrain de Recherche en Informatique et ses Applications 4
Technical University of Darmstadt 4
New University of Lisbon 4
University of Aarhus 4
University of Cambridge 4
University of Kent 4
Nokia Bell Labs 4
University of Amsterdam 4
Simon Fraser University 4
University of Copenhagen 4
University of Kiel 4
Academy of Sciences of the Czech Republic (Avcr.Cz) 4
Queen Mary, University of London 4
University of Trento 4
Humboldt University of Berlin 4
Stanford University 4
Swiss Federal Institute of Technology, Zurich 4
University of Freiburg 4
University of California, Berkeley 4
University of Texas at Austin 4
Vrije Universiteit Brussel 4
Technical University of Madrid 4
Radboud University Nijmegen 5
Ca' Foscari University of Venice 5
University of New South Wales 5
University of Houston 5
Tsinghua University 5
Aix Marseille Universite 5
University of Liege 5
University of Illinois at Urbana-Champaign 5
Bremen University 5
University of Ferrara 5
Ecole Polytechnique 5
University of Insubria 5
Western Sydney University 5
University of Alberta 5
University of Athens 5
Technical University of Munich 5
Free University of Bozen-Bolzano 5
University of Pennsylvania 5
Adam Mickiewicz University in Poznan 5
McGill University 5
University of California, San Diego 6
University of Udine 6
University of Padua 6
Max Planck Institute for Informatics 6
Swansea University 6
University of Helsinki 6
University of Verona 6
University of Bath 6
University of Sheffield 7
Royal Institute of Technology 7
Birkbeck University of London 7
Cornell University 7
Complutense University of Madrid 7
Ludwig Maximilian University of Munich 7
Technion - Israel Institute of Technology 7
Gottfried Wilhelm Leibniz Universitat 8
University of Pisa 8
The University of Warwick 8
University of Liverpool 8
University of Edinburgh 9
University of Wroclaw 9
University of Naples Federico II 9
University Michigan Ann Arbor 9
Universite Paris 7- Denis Diderot 9
Imperial College London 9
King's College London 9
Microsoft Research 10
University of Manchester 10
Tel Aviv University 10
Universitat Politecnica de Catalunya 10
University of Milan 11
Eindhoven University of Technology 11
Institute of Science and Technology Austria 12
Hebrew University of Jerusalem 12
University of Warsaw 12
University of Toronto 12
University of Turin 14
University of Calabria 15
RWTH Aachen University 15
Griffith University 15
Specifications and Verification Laboratory 16
Catholic University of Leuven, Leuven 16
University of Bologna 16
Hasselt University 18
University of Maryland 21
Carnegie Mellon University 23
University of Roma La Sapienza 25
University of Oxford 29
Vienna University of Technology 61
All ACM Journals | See Full Journal Index

Search TOCL
enter search term and/or author name