Concept
Proof assistant
Related people (14)
Viktor Kuncak
Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.
Jean-Pierre Hubaux
Jean-Pierre Hubaux is a full professor at EPFL and head of the Laboratory for Data Security. Through his research, he contributes to laying the foundations and developing the tools for protecting privacy in today’s hyper-connected world. He has pioneered the areas of privacy and security in mobile/wireless networks and in personalized health. He is the academic director of the Center for Digital Trust (C4DT). He leads the Data Protection in Personalized Health (DPPH) project funded by the ETH Council and is a co-chair of the Data Security Work Stream of the Global Alliance for Genomics and Health (GA4GH). From 2008 to 2019 he was one of the seven commissioners of the Swiss FCC. He is a Fellow of both IEEE (2008) and ACM (2010). Recent awards: two of his papers obtained distinctions at the IEEE Symposium on Security and Privacy in 2015 and 2018. He is among the most cited researchers in privacy protection and in information security. Spoken languages: French, English, German, Italian
Christian Enz
Christian C. Enz (M84, S'12) received the M.S. and Ph.D. degrees in Electrical Engineering from the EPFL in 1984 and 1989 respectively. From 1984 to 1989 he was research assistant at the EPFL, working in the field of micro-power analog IC design. In 1989 he was one of the founders of Smart Silicon Systems S.A. (S3), where he developed several low-noise and low-power ICs, mainly for high energy physics applications. From 1992 to 1997, he was an Assistant Professor at EPFL, working in the field of low-power analog CMOS and BiCMOS IC design and device modeling. From 1997 to 1999, he was Principal Senior Engineer at Conexant (formerly Rockwell Semiconductor Systems), Newport Beach, CA, where he was responsible for the modeling and characterization of MOS transistors for the design of RF CMOS circuits. In 1999, he joined the Swiss Center for Electronics and Microtechnology (CSEM) where he launched and lead the RF and Analog IC Design group. In 2000, he was promoted Vice President, heading the Microelectronics Department, which became the Integrated and Wireless Systems Division in 2009. He joined the EPFL as full professor in 2013, where he is currently the director of the Institute of Microengineering (IMT) and head of the Integrated Circuits Laboratory (ICLAB).He is lecturing and supervising undergraduate and graduate students in the field of Analog and RF IC Design at EPFL. His technical interests and expertise are in the field of very low-power analog and RF IC design, semiconductor device modeling, and inexact and error tolerant circuits and systems.He has published more than 200 scientific papers and has contributed to numerous conference presentations and advanced engineering courses. Together with E. Vittoz and F. Krummenacher he is one of the developer of the EKV MOS transistor model and the author of the book "Charge-Based MOS Transistor Modeling - The EKV Model for Low-Power and RF IC Design" (Wiley, 2006). He has been member of several technical program committees, including the International Solid-State Circuits Conference (ISSCC) and European Solid-State Circuits Conference (ESSCIRC). He has served as a vice-chair for the 2000 International Symposium on Low Power Electronics and Design (ISLPED), exhibit chair for the 2000 International Symposium on Circuits and Systems (ISCAS) and chair of the technical program committee for the 2006 European Solid-State Circuits Conference (ESSCIRC). Since 2012 he has been elected as member of the IEEE Solid-State Circuits Society (SSCS) Administrative Commmittee (AdCom). He is also Chair of the IEEE SSCS Chapter of Switzerland.
Rachid Guerraoui
Rachid Guerraoui has been affiliated with Ecole des Mines of Paris, the Commissariat à l'Energie Atomique of Saclay, Hewlett Packard Laboratories and the Massachusetts Institute of Technology. He has worked in a variety of aspects of distributed computing, including distributed algorithms and distributed programming languages. He is most well known for his work on (e-)Transactions, epidemic information dissemination and indulgent algorithms.
He co-authored a book on Transactional Systems (Hermes) and a book on reliable distributed programming (Springer). He was appointed program chair of ECOOP 1999, ACM Middleware 2001, IEEE SRDS 2002, DISC 2004 and ACM PODC 2010.
His publications are available at http://lpdwww.epfl.ch/rachid/papers/generalPublis.html
Jean-Yves Le Boudec
Jean-Yves Le Boudec is full professor at EPFL and fellow of the IEEE. He graduated from Ecole Normale Superieure de Saint-Cloud, Paris, where he obtained the Agregation in Mathematics in 1980 (rank 4) and received his doctorate in 1984 from the University of Rennes, France. From 1984 to 1987 he was with INSA/IRISA, Rennes. In 1987 he joined Bell Northern Research, Ottawa, Canada, as a member of scientific staff in the Network and Product Traffic Design Department. In 1988, he joined the IBM Zurich Research Laboratory where he was manager of the Customer Premises Network Department. In 1994 he joined EPFL as associate professor. His interests are in the performance and architecture of communication systems. In 1984, he developed analytical models of multiprocessor, multiple bus computers. In 1990 he invented the concept called "MAC emulation" which later became the ATM forum LAN emulation project, and developed the first ATM control point based on OSPF. He also launched public domain software for the interworking of ATM and TCP/IP under Linux. He proposed in 1998 the first solution to the failure propagation that arises from common infrastructures in the Internet. He contributed to network calculus, a recent set of developments that forms a foundation to many traffic control concepts in the internet. He earned the Infocom 2005 Best Paper award, with Milan Vojnovic, for elucidating the perfect simulation and stationarity of mobility models, the 2008 IEEE Communications Society William R. Bennett Prize in the Field of Communications Networking, with Bozidar Radunovic, for the analysis of max-min fairness and the 2009 ACM Sigmetrics Best Paper Award, with Augustin Chaintreau and Nikodin Ristanovic, for the mean field analysis of the age of information in gossiping protocols. He is or has been on the program committee or editorial board of many conferences and journals, including Sigcomm, Sigmetrics, Infocom, Performance Evaluation and ACM/IEEE Transactions on Networking. He co-authored the book "Network Calculus" (2001) with Patrick Thiran and is the author of the book "Performance Evaluation of Computer and Communication Systems" (2010).