Iliano Cervesato is a computer scientist and Teaching Professor in the Computer Science Department of Carnegie Mellon University (CMU) in Pittsburgh, Pennsylvania. His research spans computational logic, programming languages and computer security, and he has published more than 100 papers in these areas.
With his doctoral advisor Frank Pfenning, Cervesato developed the Linear Logical Framework (LLF), an extension of the LF logical framework with linear types; their 1996 paper introducing it received the LICS Test-of-Time Award in 2016. He later co-developed the Concurrent Logical Framework (CLF) and MSR, a multiset-rewriting formalism for specifying cryptographic protocols, and was a member of the team that in 2005 discovered a man-in-the-middle attack on PKINIT, the public-key extension of the Kerberos authentication protocol. The discovery led the Internet Engineering Task Force (IETF) to change the PKINIT specification and Microsoft to release a security update for several versions of Windows.
Cervesato taught at Carnegie Mellon University in Qatar from 2006 to 2016, where he created Discovering Logic, a first-year course built around the graphic novel Logicomix. Since 2016 he has taught 15-122 Principles of Imperative Computation, a core introductory course in CMU's computer science curriculum, on the Pittsburgh campus. He is also the author of the monograph The Deductive Spreadsheet (Springer, 2013).

Education
Cervesato studied computer science at the University of Udine in Italy from 1986, receiving a laurea in Scienze dell'Informazione (computer science) on March 7, 1991. His undergraduate thesis, written in Italian, proposed adding meta-representation capabilities to a logic programming language. From September 1990 he also studied at the University of Houston in Texas, earning a Master of Science in computer science on August 20, 1992, with a thesis on a Warren Abstract Machine implementation of the meta-logic programming language 'Log. His earliest publications, from 1991 to 1993, dealt with 'Log (with Gianfranco Rossi) and with the specification and enforcement of dynamic integrity constraints in databases (with Christoph F. Eick).
Cervesato began doctoral studies in computer science at the University of Turin in November 1991. From April 1994 to November 1995 he was an extended visitor at CMU's Computer Science Department, where he carried out his dissertation research under the supervision of Frank Pfenning. He received his PhD (Dottorato di Ricerca in Informatica) from Turin on October 16, 1996, with the dissertation A Linear Logical Framework. In 1996 he also spent several months visiting the Department of Mathematics at the Technical University of Darmstadt in Germany.

Career

Postdoctoral research
After completing his doctoral research, Cervesato remained at CMU as a postdoctoral research affiliate in the Computer Science Department until August 1997. From September 1997 to September 1999 he was a postdoctoral research affiliate in the Department of Computer Science at Stanford University. There he worked on the Pleiades project, an Office of Naval Research-funded multi-university research initiative on assurance for modular and mobile code, and co-edited the project's collected reports with John C. Mitchell. While at Stanford he taught a graduate course on linear logic and its applications in the winter quarter of 1999.

Naval Research Laboratory
From October 1999 to October 2004, Cervesato was a research scientist with the Advanced Engineering and Sciences Division of ITT Industries, working in support of the Formal Methods Section of the United States Naval Research Laboratory (NRL) in Washington, D.C. At NRL he collaborated with Catherine Meadows and Paul Syverson on the formal analysis of cryptographic protocols. During this period he was also a visiting research collaborator in the Department of Computer Science at Princeton University (2002–2004) and, in July 2003, a visiting fellow in the Department of Computer Engineering at Chulalongkorn University in Bangkok, Thailand. From 1999 to 2004 he took part in a cooperative program on logical methods for the formal verification of software, jointly supported by the National Science Foundation and the Japan Society for the Promotion of Science.

Deductive Solutions, Tulane and George Mason
In July 2004 Cervesato founded Deductive Solutions, based in Annandale, Virginia, where he served as chief research scientist. His work on a "deductive spreadsheet" during this period was funded by a DARPA grant (2004–2005). He was a visiting research collaborator in the Department of Mathematics at the University of Pennsylvania from October 2004 to January 2005, a visiting research professor in the Mathematics Department of Tulane University in New Orleans from November 2004 to November 2005, and an adjunct professor in the Department of Information and Software Engineering at George Mason University in the spring of 2006, where he taught a course on secure electronic commerce.

Carnegie Mellon University in Qatar
In July 2006 Cervesato joined the computer science teaching faculty of Carnegie Mellon University in Qatar (CMU-Q) in Doha as an associate professor, and was promoted to professor in July 2014. Over the following decade he taught a wide range of courses there (see Teaching) and led or co-led research projects funded by the Qatar National Research Fund (QNRF) and the Qatar Foundation on topics including cryptographic protocol analysis, formal reasoning about languages for distributed computation, programming for large distributed ensembles, hypervisor integrity and automated data inference for end users. According to his curriculum vitae, the grants he has held over his career total about US$7.1 million.
Cervesato organized several international computer science meetings held in Doha. He was program chair of the 12th Asian Computing Science Conference (ASIAN 2007), chair of the security and information assurance track of the 6th ACS/IEEE International Conference on Computer Systems and Applications (AICCSA 2008), co-organizer of the 2nd Annual Doha Conference on Applied Mathematics and Computational Science (2008), and general chair of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2008). Within CMU-Q he chaired the campus research committee (2009–2010) and the computer science faculty recruitment committee, and maintained the computer science program's website.

Carnegie Mellon University, Pittsburgh
In September 2016 Cervesato moved to CMU's Pittsburgh campus as a Teaching Professor in the Computer Science Department. He served on the university's Faculty Senate from 2017 to 2019, and since the fall of 2025 has been the faculty advisor of the development team for Autolab, an autograding platform.

Research
Cervesato's research concerns the logical foundations of computation and their application to programming languages, concurrency and security. On his website he compares his approach to that of a particle physicist, who studies the basic constituents of matter in order to develop new processes and materials, describing his aim as identifying the principles that govern large classes of computational problems and using them to derive effective algorithms. His curriculum vitae lists 123 refereed publications written with about 50 co-authors.

Linear logical frameworks
A logical framework is a meta-language for representing and reasoning about deductive systems such as logics and programming languages. In his doctoral work with Frank Pfenning, Cervesato designed LLF, a conservative extension of the LF logical framework whose underlying type theory, λΠ⊸&⊤, adds connectives of linear logic to LF's dependent types. Because linear hypotheses must be used exactly once, the framework allows systems involving state to be represented naturally and concisely. The paper introducing LLF, presented at the 1996 Symposium on Logic in Computer Science (LICS) in New Brunswick, New Jersey, illustrated the framework by encoding a version of Mini-ML with references (including its type system, operational semantics and a proof of type preservation) and a sequent calculus for classical linear logic together with its cut-elimination theorem. It also gave LLF an operational reading as a logic programming language. An extended version appeared in Information and Computation in 2002.
In 2016 the LICS 1996 paper received the LICS Test-of-Time Award, which recognizes papers from the symposium twenty years earlier that have proved influential; it shared that year's award with a paper by Parosh Abdulla, Karlis Cerans, Bengt Jonsson and Yih-Kuen Tsay. The award committee described LLF as one of the first logical frameworks to build linearity directly into the framework and the first to do so using an LF-style dependently typed lambda calculus, noting its use in formalizing the metatheory of imperative programming languages and its relevance to newer areas such as quantum programming languages. Later researchers have likewise identified LLF as the first system to combine linear and dependent types, and as the original work in the tradition that keeps linear and unrestricted assumptions in separate contexts.
Cervesato and Pfenning also studied higher-order unification for linear type theories (LICS 1997) and a "spine" representation of linear terms suited to implementation (Journal of Logic and Computation, 2003). With Joshua Hodas and Pfenning, Cervesato developed techniques for efficiently managing linear resources during proof search in linear logic programming languages (Theoretical Computer Science, 2000).
Beginning in 2001, Cervesato, Pfenning, Kevin Watkins and David Walker developed the Concurrent Logical Framework (CLF), which extends LF with linear types for representing state, as in LLF, together with a monad for representing concurrency. CLF was later implemented by Anders Schack-Nielsen and Carsten Schürmann as the Celf system, which has been used to encode examples such as Concurrent ML, the π-calculus, security protocols and Petri nets. Cervesato's subsequent work has addressed meta-reasoning about CLF specifications, such as matching concurrent execution traces (2012), and applications including the formalization of automated trading systems in a concurrent linear framework (2018).

Security protocol analysis
At Stanford, Cervesato worked with Nancy Durgin, Patrick Lincoln, John C. Mitchell and Andre Scedrov on MSR, a formalism based on multiset rewriting and linear logic for specifying cryptographic protocols. Their 1999 paper "A Meta-Notation for Protocol Analysis", presented at the 12th IEEE Computer Security Foundations Workshop in Mordano, Italy, used MSR to state the assumptions of the Dolev–Yao model of an intruder. It represented the generation of fresh values such as keys and nonces through existential quantification, and identified a class of theories corresponding to protocols of finite length that may run an unbounded number of instances of each role. The group subsequently related MSR to the strand-space model of protocol analysis (2000; journal version 2005).
Cervesato went on to develop a typed version of MSR with dependent types and subsorting, and published a short LICS 2001 paper titled "The Dolev–Yao Intruder Is the Most Powerful Attacker". He also related MSR to process algebras (with Stefano Bistarelli, Gabriele Lenzini and Fabio Martinelli, 2005) and represented it in an extension of rewriting logic with dependent types (with Mark-Oliver Stehr, 2007). With Paul Syverson he wrote "The Logic of Authentication Protocols", a tutorial chapter based on lectures at the 2000 FOSAD summer school.
At NRL, working with Catherine Meadows and Paul Syverson, he specified the requirements of the Group Domain of Interpretation (GDOI) group key-management protocol in the NPATRL requirements language and analyzed the protocol with the NRL Protocol Analyzer (ACM CCS 2001; Journal of Computer Security, 2004). With Meadows he also developed a fault-tree representation of NPATRL security requirements (IEEE Transactions on Dependable and Secure Computing, 2007).

Kerberos and PKINIT
Beginning in 2002, Cervesato, Frederick Butler, Aaron D. Jaggard and Andre Scedrov used MSR to carry out a formal analysis of Kerberos 5, verifying confidentiality and authentication properties of the protocol (CSFW 2002; Theoretical Computer Science, 2006).
In 2005, while extending this analysis to PKINIT, the extension that allows Kerberos to use public-key cryptography for initial authentication, Cervesato, Jaggard, Scedrov, Joe-Kai Tsay and Christopher Walstad discovered a man-in-the-middle attack against the public-key encryption mode of the protocol as specified in the IETF drafts of the time. The flaw allowed an attacker to impersonate the key distribution center and end-servers to a client, breaking the authentication guarantees of Kerberos. The team worked with the IETF Kerberos working group to correct the specification; the resulting standard, RFC 4556 (2006), credits them with discovering a binding problem between the request and reply messages in draft 26 and records that a checksum field was added as a result. Microsoft addressed the vulnerability (CAN-2005-1982) in security bulletin MS05-042 in August 2005, acknowledging the team. The researchers also formally verified several possible fixes, including the one adopted by the IETF, and, with Michael Backes, gave cryptographically sound security proofs for basic and public-key Kerberos (ESORICS 2006; International Journal of Information Security, 2011).

Temporal reasoning and the event calculus
In the 1990s, working with Angelo Montanari, Luca Chittaro and Massimo Franceschet of the University of Udine, Cervesato studied the event calculus, a logic-based formalism for reasoning about events and their effects over time. Their work introduced modal variants of the event calculus, analyzed the complexity of model checking in these calculi and surveyed extensions of the formalism (Journal of Logic Programming, 1999; Computational Intelligence, 2000). Cervesato also maintained an online bibliography of the event calculus.

The deductive spreadsheet
From 2004 Cervesato worked on the deductive spreadsheet, an extension of the traditional spreadsheet intended to let users without training in computer science reason about symbolic data in the same simple way they use spreadsheets to make decisions about numbers. The work began with DARPA funding in 2004–2005; his NEXCEL prototype project ran until 2016. It produced an article in The Knowledge Engineering Review (2007) and the monograph The Deductive Spreadsheet (Springer, 2013). The first half of the book develops a formal model of the traditional spreadsheet and extends it with relational operators and a logic-programming-based inference engine; the second half designs a user interface using methods from cognitive psychology, namely the attention investment model and the cognitive dimensions of notations. In 2005 he co-organized the first Workshop on Logical Spreadsheets at Stanford with Michael Kassoff and Michael Genesereth. A related study with Shikar Kumar and Coty Gonzalez examined how people carry out relational reasoning (Computers in Human Behavior, 2014).

Distributed and concurrent programming
At CMU-Q, Cervesato and his postdoctoral researcher Edmund S. L. Lam developed rule-based languages for programming ensembles of distributed devices, extending Constraint Handling Rules and multiset rewriting with comprehension patterns. Their work produced Comingle, a distributed logic-programming language for decentralized ensembles of mobile devices (COORDINATION 2015), along with compilation techniques for such languages. A 2016 paper on the choreographic compilation of decentralized comprehension patterns, written with Lam and Ali Elgazar, received the best paper award at the 10th International Web Rule Symposium (RuleML 2016), according to his curriculum vitae. With Scedrov he related state-based and process-based models of concurrency through linear logic (Information and Computation, 2009), and with Yuxin Deng and Robert J. Simmons he compared reasoning methodologies in linear logic and process algebra (Mathematical Structures in Computer Science, 2014).

Other research
Other projects led by Cervesato include QWeSST, a type-safe programming model for web applications developed with Thierry Sans; VirtuallySafe, a framework for hypervisor code and data integrity; and "The Garbled Computer", a project on computing without seeing the data being processed. Related systems-security work with Ryan Riley and others examined memory permissions as a protection against cross-layer attacks (ACM Transactions on Architecture and Code Optimization, 2016) and the detection of kernel-level rootkits using hardware performance counters (ASIACCS 2017). He has also applied multiset rewriting to the representation of biological systems (2003).

Teaching
As of December 2025, Cervesato's curriculum vitae listed 13 regular courses and 58 course offerings, including two new courses of his own design, as well as six invited tutorials and advanced courses.

Principles of Imperative Computation (15-122)
Since fall 2016 Cervesato has taught 15-122 Principles of Imperative Computation every fall and spring semester, as well as in the summer of 2020. The course, a core requirement of CMU's computer science major, teaches imperative programming together with methods for ensuring that programs are correct, such as function contracts and loop invariants, and applies them to fundamental data structures and algorithms. Much of the course is conducted in C0, a subset of C designed to be amenable to verification, with a transition to full C near the end. The course was originally designed by Frank Pfenning and is taken by several hundred students each year. Cervesato is a co-author of the course's lecture notes, and in 2018 he received a ProSEED/Simon Initiative grant to customize the course's learning activities for closer alignment with its learning objectives. The CMU Computer Science Department describes the course as teaching students to develop correct code quickly using fundamental data structures.

Discovering Logic
In spring 2010 Cervesato introduced Discovering Logic (15-199) at CMU-Q, a half-semester elective introducing logic to first-year computer science students. The course was built around Logicomix (2009), a graphic novel by Apostolos Doxiadis and Christos Papadimitriou about Bertrand Russell and the search for the foundations of mathematics, which Cervesato adopted as the primary text even though it had not been written as a textbook. Besides teaching elementary logic, the course aimed to develop students' communication skills and to give them historical perspective on logic and computer science, with students researching and presenting topics drawn from the book. Explaining the rationale for the course, Cervesato said that without logic, students "would know the 'how' without knowing the 'why'".
Although the course was offered only to first-year computer science majors, it attracted interest from students across the campus. Cervesato described the course in a 2011 paper at the ACM ITiCSE conference and taught it six times between 2010 and 2015. Its use of Logicomix as a primary textbook was also noted by The Daily Northwestern.

Other courses
At CMU-Q, Cervesato regularly taught 15-212 Principles of Programming (2006–2012), 15-150 Principles of Functional Programming (2012–2015), 15-312 Foundations of Programming Languages (2007–2015), 15-317 Constructive Logic and 15-349 Introduction to Computer and Network Security. He also taught Technical Writing for Computer Scientists, Technology and Global Development and 80-211 Logic and Mathematical Inquiry. Earlier in his career he taught a graduate course on linear logic and its applications at CMU (spring 1995) and at Stanford (winter 1999), and a course on secure electronic commerce at George Mason University (2006).
He has given invited tutorials on security protocol specification languages at the 2001 International School on Foundations of Security Analysis and Design (FOSAD) in Bertinoro, Italy; on linear logic and security at the 2003 Summer School on Foundations of Security in Eugene, Oregon; on cryptography and computer security at Chiang Mai University in Thailand (2003); and on logical frameworks at Université Laval in Quebec (1998), among others.

Education-related service and advising
Cervesato chaired the Education Committee of the ACM Special Interest Group on Logic and Computation (SIGLOG) from 2014 to 2016 and has remained a member of the committee since 2017. He co-authored work on teaching communication skills to computer science undergraduates (SIGCSE 2011; ITiCSE 2011) and wrote on teaching programming languages with a wiki (2008).
He has served on the doctoral thesis committees of Vivek Nigam (École polytechnique, 2009), Robert J. Simmons (CMU, 2010), Ye Wu (Stevens Institute of Technology, 2010), Agata Murawska (IT University of Copenhagen, 2017) and Henry DeYoung (CMU, 2020), and has supervised the postdoctoral researchers Thierry Sans, Jorge Luis Sacchini, Edmund S. L. Lam and Dragiša Žunić.

Professional service
Cervesato has served as program chair or general chair of thirteen international scientific conferences and workshops. He was general chair of the 14th and 15th IEEE Computer Security Foundations Workshops (CSFW-14 in 2001 and CSFW-15 in 2002, both held in Cape Breton, Nova Scotia) and of LPAR 2008 in Doha. He was program chair of the Foundations of Computer Security workshops held with FLoC 2002 in Copenhagen and LICS 2003 in Ottawa, of ASIAN 2007, of the International Workshop on Linearity (2014 and 2016), of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2015), and of the first International Workshop on Focusing (2015), held in Suva, Fiji.
He sat on the steering committee of the IEEE Computer Security Foundations Symposium (formerly Workshop) from 2001 to 2016, and has served on the steering committees of LFMTP and of the International Workshop on Linearity since 2015. His curriculum vitae lists 78 program committee memberships, including the ACM Conference on Computer and Communications Security (2008 and 2009) and the International Conference on Logic Programming (2014).
As an editor, he edited the proceedings of ASIAN 2007 and of LPAR 2008 (the latter with Helmut Veith and Andrei Voronkov) in Springer's Lecture Notes in Computer Science series, and guest-edited special issues of Mathematical Structures in Computer Science, the Journal of Automated Reasoning and the International Journal of Information Security.

Awards and honors
2016 – LICS Test-of-Time Award, with Frank Pfenning, for "A Linear Logical Framework" (LICS 1996)
2016 – Best paper award, 10th International Web Rule Symposium (RuleML 2016), with Edmund S. L. Lam and Ali Elgazar, for "Choreographic Compilation of Decentralized Comprehension Patterns"
2005–2006 – Acknowledged in Microsoft Security Bulletin MS05-042 and in RFC 4556 for the discovery of the PKINIT vulnerability, with Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay and Christopher Walstad

Other activities
Beyond his research, Cervesato has written software to support teaching and academic administration, including a web application that lets students graph their grades, observe trends and forecast outcomes, a course planner, a university-wide class scheduler and a publication manager, as well as autograding support for Standard ML assignments on Autolab. Early in his career he maintained the CMU Linear Logic Bibliography (1995–1997). In June 2012 he discussed the Flame computer virus on Qatar Foundation radio.

Selected publications
Book
Cervesato, Iliano (2013). The Deductive Spreadsheet. Cognitive Technologies. Springer. doi:10.1007/978-3-642-37747-1. ISBN 978-3-642-37746-4.
Journal articles and conference papers
Cervesato, Iliano; Pfenning, Frank (1996). A Linear Logical Framework. Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS '96). pp. 264–275.
Cervesato, Iliano; Durgin, Nancy A.; Lincoln, Patrick D.; Mitchell, John C.; Scedrov, Andre (1999). A Meta-Notation for Protocol Analysis. 12th IEEE Computer Security Foundations Workshop (CSFW-12). pp. 55–69. doi:10.1109/CSFW.1999.779762.
Cervesato, Iliano; Montanari, Angelo (1999). "A General Modal Framework for the Event Calculus and Its Skeptical and Credulous Variants". Journal of Logic Programming. 38 (2): 111–164. doi:10.1016/S0743-1066(98)10021-3.
Cervesato, Iliano; Hodas, Joshua S.; Pfenning, Frank (2000). "Efficient Resource Management for Linear Logic Proof Search". Theoretical Computer Science. 232 (1–2): 133–163. doi:10.1016/S0304-3975(99)00173-5.
Syverson, Paul; Cervesato, Iliano (2001). "The Logic of Authentication Protocols". Foundations of Security Analysis and Design. Lecture Notes in Computer Science. Vol. 2171. Springer. pp. 63–136.
Cervesato, Iliano (2001). The Dolev–Yao Intruder Is the Most Powerful Attacker. Sixteenth Annual Symposium on Logic in Computer Science (LICS '01). Boston, MA.
Cervesato, Iliano; Pfenning, Frank (2002). "A Linear Logical Framework". Information and Computation. 179 (1): 19–75. doi:10.1006/inco.2001.2951.
Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David (2002). A Concurrent Logical Framework I: Judgments and Properties (Technical report). Carnegie Mellon University. CMU-CS-02-101.
Cervesato, Iliano; Pfenning, Frank (2003). "A Linear Spine Calculus". Journal of Logic and Computation. 13 (5): 639–688. doi:10.1093/logcom/13.5.639.
Cervesato, Iliano; Durgin, Nancy; Lincoln, Patrick D.; Mitchell, John C.; Scedrov, Andre (2005). "A Comparison between Strand Spaces and Multiset Rewriting for Security Protocol Analysis". Journal of Computer Security. 13 (2): 265–316. doi:10.3233/JCS-2005-13203.
Butler, Frederick; Cervesato, Iliano; Jaggard, Aaron D.; Scedrov, Andre; Walstad, Christopher (2006). "Formal Analysis of Kerberos 5". Theoretical Computer Science. 367 (1–2): 57–87. doi:10.1016/j.tcs.2006.08.040.
Cervesato, Iliano (2007). "NEXCEL, a Deductive Spreadsheet". The Knowledge Engineering Review. 22 (3): 221–236. doi:10.1017/S0269888907001142.
Cervesato, Iliano; Jaggard, Aaron D.; Scedrov, Andre; Tsay, Joe-Kai; Walstad, Christopher (2008). "Breaking and Fixing Public-Key Kerberos". Information and Computation. 206 (2–4): 402–424. doi:10.1016/j.ic.2007.05.005.
Cervesato, Iliano; Scedrov, Andre (2009). "Relating State-Based and Process-Based Concurrency through Linear Logic". Information and Computation. 207 (10): 1044–1077. doi:10.1016/j.ic.2008.11.006.
Cervesato, Iliano (2011). Discovering Logic through Comics. ITiCSE '11. ACM. pp. 103–107. doi:10.1145/1999747.1999778.
Edited volumes
Cervesato, Iliano, ed. (2007). Advances in Computer Science – ASIAN 2007: Computer and Network Security. Lecture Notes in Computer Science. Vol. 4846. Springer.
Cervesato, Iliano; Veith, Helmut; Voronkov, Andrei, eds. (2008). Logic for Programming, Artificial Intelligence, and Reasoning: 15th International Conference, LPAR 2008. Lecture Notes in Computer Science. Vol. 5330. Springer.

See also
Linear logic
Logical framework
Twelf
Dolev–Yao model
Kerberos (protocol)
Logicomix

References

External links
Official website
Faculty profile, Computer Science Department, Carnegie Mellon University