Welcome to João Marques Silva's Home Page

		Research		Professional Activities		Graduate Supervision
		Teaching		Undergraduate Supervision		Utilities and Links

I'm an Associate Professor (with Agregação) at Departamento de Engenharia Informática (Informatics Department) (DEI), Instituto Superior Técnico (IST), Universidade Técnica de Lisboa (UTL), and a Senior Researcher at Instituto de Engenharia de Sistemas e Computadores -- Research & Development Lisbon (INESC-ID), coordinating the research group Software Algorithms and Tools for constraint solving (SAT).

Contact

Instituto de Engenharia de Sistemas e Computadores (INESC-ID) R. Alves Redol, 9 1000-029 Lisboa, Portugal

351-21-310-0387 [V] 351-21-314-5843 [F]

http://sat.inesc-id.pt/~jpms jpms 'at' inesc-id.pt

Research

• My main research interests include algorithms for Boolean Satisfiability (SAT) and for Boolean Optimization, in particular Unate and Binate Covering (UCP/BCP) and 0-1 Integer Linear Programming (ILP). Additional research interests include applications of SAT, BCP and ILP in Model Checking, and in Electronic Design Automation (EDA), including Automatic Test Pattern Generation, Timing Analysis and Verification, and Logic and Functional Verification.

• Recent publications

• Complete list of publications

• Technical reports

• Tutorials

• Talks

• Projects

• Software

• I maintain a web page with information on the Propositional Satisfiability solver GRASP, and keep a web page with resources on Propositional Satisfiability.

• Research opportunities/positions.

  
  

• More updated information regarding the SAT group's research work is available from the group's web page.

• Co-Chair for the Third Workshop on Constraints in Formal Verification, to be held during the upcoming CADE'05 conference.

• Organizing committee member for the Fourth Formal Equivalence Verification Workshop (FCEV'05).

• Program committee member for the Third International Workshop on Bounded Model Checking, to be held during the upcoming CAV'05 conference.

• Program committee member for the Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT'05).

• Program committee member for the Workshop on Quantification in Constraint Programming, to be held during the upcoming CP'05 conference.

• Program committee member for the First International Workshop Constraint Programming Beyond Finite Integer Domains, to be held during the upcoming CP'05 conference.

• Member of the Editorial Board for the Journal on Satisfiability, Boolean Modeling and Computation (JSAT).

• Paulo Matos. MSc student working on Linear Arithmetic Logic.

• António Morgado. MSc student working on propositional model enumeration and counting.

• Vasco Manquinho. MSc and PhD student working on search algorithms for the Boolean Optimization. Vasco concluded his MSc in May/1999, and he is now finalizing his PhD degree.

• Elsa Carvalho. Graduate student that worked on branching heuristics for SAT. Elsa concluded her degree in Jul/2004.

• Luís Baptista. MSc student that worked on randomization and search restarts for propositional satisfiability. Luis concluded his MSc degree in Dec/2000, and currently works on applications of SAT.

• Inês Lynce. MSc and PhD student that worked on new algorithms for propositional satisfiability. Ines concluded her MSc degree in Mar/2001, and her PhD degree in Feb/2005.

• Paulo Flores. Ph.D. student that worked on models and algorithms for optimization problems for digital system testing. Paulo concluded his PhD degree in Dec/2001.

• Luís Guerra e Silva. MSc student that worked on Circuit Satisfiability and SAT-based algorithms for delay computation. Luís concluded his MSc degree in Jun/1999.

• Currently, I teach an introductory graduate level course on the Analysis and Design of Algorithms (in Portuguese),

• an introductory course on Algorithms and Data Structures (in Portuguese),

• and a graduate course on Logic in Computer Science (in Portuguese).

• In recent years I also taught courses on Computer Programming (in Portuguese), Electronic Circuits and Systems (in Portuguese), Programming in the UNIX OS at EST/IPCB (in Portuguese), Algorithms at EST/IPCB (in Portuguese), and a graduate level course on Discrete Optimization Algorithms.

• A few publications related with my teaching activity can be found here. A few lecture notes for the courses I teach can be found here.
  (These publications and lecture notes are written in Portuguese.)

• Undergraduate final project proposals for the 2005/2006 academic year (in Portuguese).

• Simplex-based linear programming package in Java.

• A prototype of a Java-based toolkit for teaching electronic circuits and systems (in Portuguese).

• SAT-based ATPG package, that has been incorporated into the Cadence design framework.

• I maintain a web page of Perl scripts, that I have written for solving different problems.

• A few old links.

• Man pages as well as tutorials and documents on different programming languages and utilities. (Due to distribution restrictions, these documents can only be made available to client machines within the IST/INESC domains.)

Personal Stuff

• A few family photos.

• Sports: Mountain Biking, Paddling, Hiking, Sailing and Tennis.

• You may also want to check my teaching schedule for the current term.

You are visitor number -- >

Page Access Information

You are visitor number to this page since Sep. 15th 2000.