Miquel Bofill Arasa

Universitat de Girona
Escola Politècnica Superior
Dept. Informàtica i Matemàtica Aplicada
Campus Montilivi, Edifici P4
E-17071 Girona - Catalunya (Spain)

 Tel. +34 972 41 88 38
 Fax +34 972 41 87 92
 Office P4-230

mbofillatima.udg.edu

Teaching

Research areas of interest

My research interest is related to logic in computer science:
  • SAT modulo theories
  • Automated Deduction (see also Automated Theorem Proving)
    		•

    Publications

    Journal Articles

    Miquel Bofill and Albert Rubio
    Paramodulation with well-founded orderings
    Journal of Logic and Computation , Vol. 19(2), April 2009
    doi: 10.1093/logcom/exn073

    Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
    Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings
    Journal of Automated Reasoning. Volume 30:1, January 2003. © Kluwer
     

    Conference Papers

    Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
    A Write-Based Solver for SAT Modulo the Theory of Arrays
    In Procs. Eighth International Conference on Formal Methods in Computer-Aided Design (FMCAD), Portland, USA, November 2008. ©2008 IEEE. This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

    Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
    The Barcelogic SMT Solver
    In Procs. 20th International Conference on Computer Aided Verification (CAV)
    LNCS 5123, pages 294-298, Princeton, USA, July 2008. © Springer-Verlag

    Miquel Bofill and Albert Rubio
    Redundancy Notions for Paramodulation with Non-Monotonic Orderings (long version) (slides)
    In Procs. Second International Joint Conference on Automated Reasoning (IJCAR)
    LNAI 3097, pages 107-121, Cork, Ireland, July 2004. © Springer-Verlag

    Miquel Bofill and Albert Rubio
    Well-foundedness is sufficient for Completeness of Ordered Paramodulation (long version) (slides)
    In Procs. 18th International Conference on Automated Deduction (CADE)
    LNAI 2392, pages 456-470, Copenhagen, Denmark, July 2002. © Springer-Verlag

    Miquel Bofill and Guillem Godoy
    On the Completeness of Arbitrary Selection Strategies for Paramodulation (long version)
    In Procs. 28th International Colloquium on Automata, Languages and Programming (ICALP)
    LNCS 2076, pages 951-962, Crete, Greece, July 2001. © Springer-Verlag

    Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
    Modular Redundancy for Theorem Proving (electronic version)
    In Procs. Third International Workshop on Frontiers of Combining Systems (FroCoS)
    LNAI 1794, pages 186-199, Nancy, France, April, 2000. © Springer-Verlag

    Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
    Paramodulation with Non-Monotonic Orderings
    In Procs. 14th Annual IEEE Symposium on Logic in Computer Science (LICS)
    pages 225-234, Trento, Italy, July, 1999. © IEEE Comp. Sc. Press

    PhD Dissertation

    Equational Reasoning with Non-Monotonic Orderings (slides)
    Technical University of Catalonia, july 2004.
    Supervisor: Albert Rubio

    The counter shows  accesses to this page since 19 feb. 2007.