Joao Marques Silva

Biography

Research Interests:

• Applied formal methods
• Artificial Intelligence
• Bioinformatics
• Decision & Optimization Procedures

General

Name and Title: 

Professor Joao Marques-Silva Habilitation PhD MSc

Position: 

Sfi Stokes Professor of Computer Science and Infor

Phone: 

+353 1 716 5700

Email: 

Personal Website: 

http://www.csi.ucd.ie/staff/jpms

Office: 

CASL / 3N

Address:
School of Computer Science & Informatics
UCD Casl
Belfield Office Park, Dublin 4

• Biography
• Professional
• Publications
• Research

Biography

Joao Marques-Silva is SFI Stokes Professor of Computer Science and Informatics, School of Computer Science and Informatics, University College Dublin, Ireland. Before joining UCD, Joao Marques-Silva held positions at the University of Southampton, UK, and at IST/Technical University of Lisbon, Portugal. Joao Marques-Silva has a BSc and a MSc from IST/Technical University of Lisbon, a PhD from the University of Michigan, and a Habilitation in Computer Science from the Technical University of Lisbon.

 

Professional

Honours & Awards:

• Year: 2009.
  Title: 2009 CAV Award

Professional Associations:

• Association: Institute of Electrical and Electronics Engineers (IEEE), Function/Role: Senior Member
• Association: Association for Computing Machinery (ACM), Function/Role: Member

Employment:

• Employer: University of Southampton
  Position: Professor of Computer Science (Sep'07 - Jan'09)
• Employer: University of Southampton
  Position: Senior Lecturer (Oct'05 - Aug'07)
• Employer: IST/Technical University of Lisbon
  Position: Associate Professor (Sep'04 - Sep'05)
• Employer: IST/Technical University of Lisbon
  Position: Assistant Professor (Oct'95 - Aug'04)

Education:

• Year 2004 Institution: European Uni Lisbon Portugal
  Qualification: HABILITATION Subject:
• Year 1995 Institution: University of Michigan
  Qualification: PhD Subject: Electrical Engineering and Computer Science
• Year 1991 Institution: IST/Technical University of Lisbon
  Qualification: MSc Subject: Electrical and Computer Engineering
• Year 1988 Institution: IST/Technical University of Lisbon
  Qualification: BSc Subject: Electrical and Computer Engineering

Publications

Book Chapters:

• J. Marques-Silva and J. Planes (2011) 'Algorithms for Maximum Satisfiability using Unsatisfiable Cores' In: Recent Advances in Logic Synthesis. Germany: Springer. [Details]
• Ana Graca, Joao Marques-Silva and Ines Lynce (2011) 'Haplotype Inference using Propositional Satisfiability' In: R. Bruni (eds). Mathematical Approaches to Polymer Sequence Analysis. Germany: Springer. [DOI] [Details]
• J. Marques-Silva (2009) 'Boolean Satisfiability and EDA Applications' In: Cambridge University Press. [Details]
• J. Marques-Silva and I. Lynce and S. Malik (2009) 'Conflict-Driven Clause Learning SAT Solvers' In: IOS Press. [Details]
• I. Lynce and V. Manquinho and J. Marques-Silva (2008) 'Backtracking' In: Wiley. [Details]
• A. Bhalla and I. Lynce and J. Sousa and J. Marques-Silva (2005) 'Heuristic-Based Backtracking Relaxation for Propositional Satisfiability' In: Springer. [Details]
• J. Marques-Silva and K. Sakallah (2003) 'GRASP - A New Search Algorithm for Satisfiability' In: Kluwer Academic Publishers. [Details]
• I. Lynce and J. Marques-Silva (2003) 'The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms' In: Springer. [Details]
• W. Kunz and J. Marques-Silva and S. Malik (2001) 'SAT and ATPG: Algorithms for Boolean Decision Problems' In: Kluwer Academic Publishers. [Details]

Books Edited:

• J. Marques-Silva and K. Sakallah (Ed.). (2007) 10th International Conference on Theory and Applications of Satisfiability Testing. Springer, LNCS 4501. [Details]

Peer Reviewed Journals:

• Lucas Cordeiro and Bernd Fischer and Joao Marques-Silva (2011) 'SMT-Based Bounded Model Checking for Embedded ANSI-C Software'. IEEE Transactions on Software Engineering, . [Details]
• Joao Marques-Silva and Josep Argelich and Ana Graça and Ines Lynce (2011) 'Boolean Lexicographic Optimization'. Annals of Mathematics and Artificial Intelligence, . [Details]
• Joao Marques-Silva (2011) 'Computing Minimally Unsatisfiable Subformulas: State of the Art and Future Directions'. Journal of Multiple-Valued Logic and Soft Computing, . [Details]
• A. Graça, J. Marques-Silva, I. Lynce and A. Oliveira (2011) 'Haplotype Inference with Pseudo-Boolean Optimization'. Annals of Operations Research, 184 (1):137-162. [DOI] [Details]
• I. Lynce and J. Marques-Silva (2011) 'Restoring CSP Satisfiability with MaxSAT'. Fundamenta Informaticae, . [Details]
• Karem A. Sakallah and Joao Marques-Silva (2011) 'Anatomy and Empirical Evaluation of Modern SAT Solvers'. Bulleting of the EATCS, 103 :96-121. [Details]
• Y. Chen, S. Safarpour, J. Marques-Silva and A. Veneris (2010) 'Automated Design Debugging with Maximum Satisfiability'. IEEE Transactions on COMPUTER-AIDED DESIGN of Integrated Circuits and Systems, 29 (11):1804-1817. [DOI] [Details]
• Antonio Morgado and Joao Marques-Silva (2010) 'Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem'. Fundamenta Informaticae, 102 (3-4):363-389. [DOI] [Details]
• Ana Graça, Ines Lynce, Joao Marques-Silva and Arlindo Oliveira (2010) 'Haplotype Inference by Pure Parsimony: a Survey'. Journal of Computational Biology, 17 (8):969-992. [DOI] [Details]
• M. Liffiton and M. Mneimneh and I. Lynce and Z. Andraus and J. Marques-Silva and K. Sakallah (2009) 'A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas'. Constraints: An International Journal, 13 (4):415-442. [Details]
• J. Marques-Silva (2008) 'Model Checking with Boolean Satisfiability'. Journal of Algorithms in Cognition, Informatics and Logic, . [Details]
• I. Lynce and J. Marques-Silva and S. Prestwich (2008) 'Boosting Haplotype Inference with Local Search'. Constraints: An International Journal, 13 (1-2):155-179. [Details]
• I. Lynce and J. Marques-Silva (2008) 'Haplotype Inference with Boolean Satisfiability'. International Journal on Artificial Intelligence Tools, 17 (2):355-287. [Details]
• I. Lynce and J.Marques-Silva (2007) 'Random Backtracking in Backtrack Search Algorithms for Satisfiability'. Discrete Applied Mathematics, 155 (12):1604-1612. [Details]
• J. Marques-Silva and K. Sakallah and I. Lynce (2007) 'Report on the SAT 2007 Conference on Theory and Applications of Satisfiability Testing'. AI Magazine, 28 (4):135-136. [Details]
• J. Marques-Silva (2007) 'Interpolant Learning and Reuse in SAT-Based Model Checking'. Electronic Notes on Theoretical Comptuer Science, 174 (3):31-43. [Details]
• V. Manquinho and J. Marques-Silva (2006) 'On Using Cutting Planes in Pseudo-Boolean Optimization'. Journal on Satisfiability, Boolean Modeling and Computation, 2 :209-219. [Details]
• A.Bhalla and I. Lynce and J. Sousa and J. Marques-Silva (2005) 'Heuristic-Based Backtracking Relaxation for Propositional Satisfiability'. Journal on Automated Reasoning, 35 (1-3):3-24. [Details]
• I. Lynce and J. Marques-Silva (2005) 'Efficient Data Structures for Backtrack Search SAT Solvers'. Annals of Mathematics and Artificial Intelligence, 43 (1-4):137-152. [Details]
• V.~Manquinho e J.~Marques-Silva (2004) 'On Solving Boolean Optimization with Satisfiability-Based Algorithms'. Annals of Mathematics and Artificial Intelligence, 40 (3-4). [Details]
• J. Marques-Silva and L. Guerra e Silva (2003) 'Solving Satisfiability in Combinational Circuits'. IEEE Design and Test of Computers, 20 (4):16-21. [Details]
• I. Lynce and J. Marques-Silva (2003) 'An Overview of Backtrack Search Satisfiability Algorithms'. Annals of Mathematics and Artificial Intelligence, 37 (3):307-326. [Details]
• V.~Manquinho and J.~Marques-Silva (2002) 'Search Pruning Techniques in SAT-Based Branch-and-Bound Algorithms for the Binate Covering Problem'. IEEE Transactions on Computer-Aided Design, 21 (5):505-516. [Details]
• L.~Guerra e Silva and J.~Marques-Silva and L.~M. Silveira and K.~Sakallah (2002) 'Satisfiability Models and Algorithms for Circuit Delay Computation'. ACM Transactions on Design Automation of Electronic Systems, 7 (1):137-158. [Details]
• P. Flores and H. Neto and J. Marques-Silva (2001) 'An Exact Solution to the Minimum-Size Test Pattern Problem'. ACM Transactions on Design Automation of Electronic Systems, 6 (4):629-644. [Details]
• A.~Oliveira e J.~Marques-Silva (2001) 'Efficient Algorithms for the Inference of Minimum Size DFAs'. Machine Learning, 44 (1-2):93-119. [Details]
• J.~Marques-Silva e K.~Sakallah (1999) 'GRASP: A Search Algorithm for Propositional Satisfiability'. IEEE Transactions on Computers, 48 (5):506-521. [DOI] [Details]
• M.~Riepe and J.~Marques-Silva and K.~Sakallah and R.~Brown (1996) 'Ravel-XL: A Hardware Accelerator for Assigned-Delay Compiled-Code Logic Gate Simulation'. IEEE Transactions on VLSI Systems, 4 (1):113-129. [Details]

Conference Publications:

• Federico Heras and Antonio Morgado and Joao Marques-Silva (2011) Core-Guided Binary Search Algorithms for Maximum Satisfiability AAAI Conference on Artificial Intelligence [Details]
• Federico Heras and Joao Marques-Silva (2011) Read-Once Resolution for Unsatisfiability-Based Max-SAT International Joint Conference on Artificial Intelligence [Details]
• Anton Belov and Joao Marques-Silva (2011) Accelerating MUS Extraction with Recursive Model Rotation Formal Methods in Computer-Aided Design Austin, Texas, USA, , 30-OCT-11 - 02-NOV-11 [Details]
• Joao Marques-Silva and Ines Lynce (2011) On Improving MUS Extraction Algorithms International Conference on Theory and Applications of Satisfiability Testing [Details]
• Mikolas Janota and Joao Marques-Silva (2011) Abstraction-Based Algorithm for 2QBF International Conference on Theory and Applications of Satisfiability Testing [Details]
• Mikolas Janota and Joao Marques-Silva (2011) {On Deciding MUS Membership with QBF International Conference on Principles and Practice of Constraint Programming [Details]
• Anton Belov and Joao Marques-Silva (2011) Minimally Unsatisfiable Boolean Circuits International Conference on Theory and Applications of Satisfiability Testing [Details]
• Mikolas Janota and Joao Marques-Silva (2011) cmMUS: A Tool for Circumscription-Based MUS Membership Testing International Conference on Logic Programming and Nonmonotonic Reasoning [Details]
• Huan Chen and Joao Marques-Silva (2011) Improvements to Satisfiability-Based Boolean Function Bi-Decomposition {International Conference on Very Large Scale Integration [Details]
• Hadi Katebi and Karem Sakallah and Joao Marques-Silva (2011) Empirical Study of the Anatomy of Modern SAT Solvers International Conference on Theory and Applications of Satisfiability Testing [Details]
• Joao Marques-Silva and Mikolas Janota and Ines Lynce (2010) On Computing Backbones of Propositional Theories European Conference on Artificial Intelligence [Details]
• M. Janota, R. Grigore and J. Marques-Silva (2010) Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription . In: T. Janhunen and I. Niemela eds. European Conference on Logics in Artificial Intelligence , pp.195-207 [DOI] [Details]
• Joao Marques-Silva (2010) Minimal Unsatisfiability: Models, Algorithms & Applications International Symposium on Multi-Valued Logic [Details]
• A. Graca, I. Lynce, J. Marques-Silva and A. Oliveira (2010) Efficient and Accurate Haplotype Inference by Combining Parsimony and Pedigree Information Algebraic and Numeric Biology [Details]
• A. Darbari, B. Fischer and J. Marques-Silva (2010) Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking International Colloquium on Theoretical Aspects of Computing Natal, Brazil, , 01-SEP-10 - 03-SEP-10 [Details]
• Lucas Cordeiro and Bernd Fischer and Joao Marques-Silva (2010) Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking Engineering of Computer-Based Systems [Details]
• M. Janota and G. Botterweck and R. Grigore and J. Marques-Silva (2010) How to Complete an Interactive Configuration Process? -- Configuring as Shopping International Conference on Current Trends in Theory and Practice of Computer Science [Details]
• Joao Marques-Silva, Josep Argelich, Ana Graca and Ines Lynce (2010) Boolean Lexicographic Optimization RCRA Workshop [Details]
• Josep Argelich and Daniel Le Berre and Ines Lynce and Joao Marques-Silva and Pascal Rapicault (2010) Solving Linux Upgradeability Problems Using Boolean Optimization Workshop on Logics for Component Configuration [Details]
• P. Matos and B. Fischer and J. Marques-Silva (2009) A Lazy Unbounded Model Checker for Event-B International Conference on Formal Engineering Methods [Details]
• Lucas Cordeiro and Bernd Fischer and Joao Marques-Silva (2009) SMT-Based Bounded Model Checking for Embedded ANSI-C Software International Conference on Automated Software Engineering [Details]
• Huan Chen and Joao Marques-Silva (2009) TG-PRO: A New Model for SAT-Based ATPG International High Level Design Validation and Test Workshop [Details]
• Ines Lynce and Joao Marques-Silva (2009) Restoring CSP Satisfiability with MaxSAT Portuguese Conference on Artificial Intelligence [Details]
• Ana Graca and Ines Lynce and Joao Marques-Silva and Arlindo Oliveira (2009) Haplotype Inference Combining Pedigrees and Unrelated Individuals Workshop on Constraint Based Methods for Bioinformatics [Details]
• Ashish Darbari and Bernd Fischer and Joao Marques-Silva (2009) Formalizing a SAT Proof Checker in Coq Coq Workshop [Details]
• Josep Argelich and Ines Lynce and Joao Marques-Silva (2009) On Solving Boolean Multilevel Optimization Problems International Joint Conference on Artificial Intelligence [Details]
• Vasco Manquinho and Joao Marques-Silva and Jordi Planes (2009) Algorithms for Weighted Boolean Optimization International Conference on Theory and Applications of Satisfiability Testing [Details]
• Yibin Chen and Sean Safarpour and Andreas Veneris and Joao Marques-Silva (2009) Spatial and Temporal Design Debug using Partial MaxSAT IEEE Great Lakes Symposium on VLSI [Details]
• Lucas Cordeiro and Bernd Fischer and Huan Chen and Joao Marques-Silva (2009) Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints IEEE International Conference on Embedded Systems and Software [Details]
• A. Morgado and J. Marques-Silva (2008) Combinatorial Optimization Solutions for the Maximum Quartet Consistency Problem RCRA Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Udine, Italy, [Details]
• A. Graca and I. Lynce and J. Marques-Silva and A. Oliveira (2008) Generic ILP vs Specialized 0-1 ILP for Haplotype Inference Workshop on Constraint Based Methods for Bioinformatics Paris, France, [Details]
• A. Morgado and J. Marques-Silva (2008) A Pseudo-Boolean Solution to the Maximum Quartet Consistency Problem Workshop on Constraint Based Methods for Bioinformatics Paris, France, [Details]
• P.~Matos and J.~Planes and F.~Letombe and J.~Marques-Silva (2008) An Algorithm Porfolio for MAX-SAT European Conference on Artificial Intelligence Patras, Greece, [Details]
• J.~Marques-Silva (2008) Practical Applications of Boolean Satisfiability Workshop on Discrete Event Systems Gothenburg, Sweden, , pp.74-80 [Details]
• A.~Graca and J.~Marques-Silva and I.~Lynce and A.~Oliveira (2008) Efficient Haplotype Inference with Combined CP and OR Techniques International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems Paris, France, , pp.308-312 [Details]
• P.~Matos and J.~Marques-Silva (2008) Model Checking Event-B by Encoding into Alloy ABZ2008 Conference London, UK, [Details]
• F.~Letombe and J.~Marques-Silva (2008) Improvements to Hybrid Incremental SAT Algorithms International Conference on Theory and Applications of Satisfiability Testing Guangzhou, China, , pp.168-181 [Details]
• J.~Marques-Silva and V.~Manquinho (2008) Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms International Conference on Theory and Applications of Satisfiability Testing Guangzhou, China, , pp.225-230 [Details]
• J.~Marques-Silva and J.~Planes (2008) Algorithms for Maximum Satisfiability using Unsatisfiable Cores Design, Automation and Test in Europe Conference and Exhibition Munich, France, , pp.408-413 [Details]
• J.~Marques-Silva and I.~Lynce and V.~Manquinho (2008) Symmetry Breaking for Maximum Satisfiability International Conference on Logic for Programming Artificial Intelligence and Reasoning Doha, Qatar, [Details]
• I.~Lynce and A. Graca and J.~Marques-Silva and A.~Oliveira (2008) Haplotype Inference with Boolean Constraint Solving: An Overview International Conference on Tools with Artificial Intelligence Dayton, Ohio, USA, [Details]
• F.~Heras and V.~Manquinho and J.~Marques-Silva (2008) On Applying Unit Propagation-Based Lower Bounds in Pseudo-Boolean Optimization International FLAIRS Conference Coconut Grove, Florida, EUA, , pp.71-76 [Details]
• N.~Bombieri and F.~Fummi and G.~Pravadelli and J.~Marques-Silva (2007) Towards Equivalence Checking Between TLM and RTL Models International Conference on Formal Methods and Models for Codesign Nice, France, , pp.113-122 [Details]
• A.~Graca and J.~Marques-Silva and I.~Lynce and A.~Oliveira (2007) Efficient Haplotype Inference with Pseudo-Boolean Optimization International Conference on Algebraic Biology Hagenberg, Austria, , pp.125-139 [Details]
• J.~Marques-Silva and I.~Lynce (2007) Towards Robust CNF Encodings of Cardinality Constraints International Conference on Principles and Practice of Constraint Programming Providence, Rhode Island, USA, , pp.483-497 [Details]
• J.~Marques-Silva and I.~Lynce and A.~Graca and A.~Oliveira (2007) Efficient and Tight Upper Bounds for Haplotype Inference by Pure Parsimony Portuguese Conference on Artificial Intelligence Guimaraes, Portugal, , pp.621-632 [Details]
• I.~Lynce and J.~Marques-Silva (2007) Breaking Symmetries in SAT Matrix Models International Conference on Theory and Applications of Satisfiability Testing Lisbon, Portugal, , pp.22-27 [Details]
• J. Marques-Silva (2006) Interpolant Learning and Reuse in SAT-Based Model Checking Bounded Model Checking Workshop Seattle, Washington, U.S.A, [Details]
• I.~Lynce and J.~Marques-Silva (2006) SAT in Bioinformatics: Making the Case with Haplotype Inference International Conference on Theory and Applications of Satisfiability Testing Seattle, Washington, USA, , pp.136-141 [Details]
• O. Kullmann and I.~Lynce and J.~Marques-Silva (2006) Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel International Conference on Theory and Applications of Satisfiability Testing Seattle, Washington, USA, , pp.22-35 [Details]
• I.~Lynce and J.~Marques-Silva (2006) Efficient Haplotype Inference with Boolean Satisfiability AAAI Conference on Artificial Intelligence Boston, Massachusetts, USA, , pp.104-109 [Details]
• A.~Morgado and P.~Matos and V.~Manquinho and J.~Marques-Silva (2006) Counting Models in Integer Domains International Conference on Theory and Applications of Satisfiability Testing Seattle, Washington, USA, , pp.410-423 [Details]
• V.~Manquinho and J.~Marques-Silva (2005) Effective Lower Bounding Techniques for Pseudo-Boolean Optimization Design, Automation and Test in Europe Conference Munich, Germany, , pp.660-665 [Details]
• V.~Manquinho and J.~Marques-Silva (2005) On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization International Conference on Theory and Applications of Satisfiability Testing St.~Andrews, UK, , pp.451-458 [Details]
• J.~Marques-Silva (2005) Improvements to the Implementation of Interpolant-Based Model Checking Conference on Correct Hardware Design and Verification Methods Saarbrucken, Germany, , pp.367-370 [Details]
• A.~Morgado and J.~Marques-Silva (2005) Good Learning and Implicit Model Enumeration International Conference on Tools with Artificial Intelligence Hong Kong, China, , pp.131-136 [Details]
• V.~Manquinho and J.~Marques~Silva (2005) Satisfiability-Based Algorithms for Pseudo-Boolean Optimization Using Gomory Cuts and Search Restarts International Conference on Tools with Artificial Intelligence Hong Kong, China, , pp.150-155 [Details]
• M.~Mneimneh and I.~Lynce and Z.~Andraus and J.~Marques~Silva and K.~Sakallah (2005) A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas International Conference on Theory and Applications of Satisfiability Testing St.~Andrews, UK, , pp.467-474 [Details]

Dissertations/Theses

• J. Marques-Silva (1995) Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. Dissertations/Theses [Details]

Research

Research Interests:

Decision and optimization procedures, including Boolean satisfiability and extensions. Applied formal methods. Applications in system verification and model checking, artificial intelligence, design automation, and bioinformatics.