CyberSlug University of California at Santa Cruz


Jack Baskin School of Engineering



Faculty

avg
@
cs.ucsc.edu

Office: E2-355 (831)459-4611
ALLEN VAN GELDER


Professor of Computer Science

Education:
B.S., Mathematics, Massachusetts Institute of Technology
Ph.D., Computer Science, Stanford University
Allen Van Gelder photo


Allen Van Gelder's research interests include development of algorithms for propositional satisfiability and quantified boolean formulas, methods for verifiable software, theorem proving, analysis of algorithms, parallel algorithms, computer graphics, and scientific visualization. He received a National Science Foundation Presidential Young Investigator Award in 1989 to investigate the use of logic programming for problems in database and artificial intelligence systems.


Office Hours, Fall 2022: avg @ cs.ucsc.edu


  MW 4:00 -- 5:00 plus appt. or drop-in

CSE016 Fall22 web page
  Applied Discrete Mathematics   Media Theatre M110
  MWF 2:40 -- 3:45
  Main Text: Hammack   Book of Proof 3RD EDITION, Hardback, softback, pdf all available
There will be a REVIEW QUIZ for CSE 016 during the FIRST CLASS MEETING.
REVIEW , REVIEW , REVIEW !!

Teaching Assts.:
   Sukhveer Karlcut (skarlcut@ucsc.edu),
  icolas Tee (\texttt{ntee@ucsc.edu}),
  revor Weger (\texttt{teweger@ucsc.edu})
Catalog entry:

OLDER CLASS WEB PAGES MIGHT BE INACCESSIBLE; email me if you need access.

CSE103 Winter22 Section 02 web page
  Computational Models
  Changed to remote
  Originally Merrill Academic 102
  MWF 1:20 -- 2:25
  Main Text: Hopcroft, Motwani, Ullman 3RD EDITION   Automata Theory, Languages, and Computation, Hardback, pdf also available
There will be a REVIEW QUIZ for CSE 101 during the FIRST CLASS MEETING.
REVIEW , REVIEW , REVIEW !!

Catalog entry:
Various representations for regular languages, context-free grammars, normal forms, simple parsing, pumping lemmas, Turing machines, the Church-Turing thesis, intractable problems, the P-NP question. (Formerly CMPS 130.) Prerequisite: Prerequisite(s): CSE 101.

CSE107 Winter21 web page
  Probability and Statistics for Engineers

CSE102 Winter20-02 web page
  Introduction to Analysis of Algorithms

CSE102 Fall 2019 web page
  Introduction to Analysis of Algorithms

NOTE: Earlier classes use CMPS not CSE.

CMPS 102 Spring 2019 web page
  Introduction to Analysis of Algorithms

CMPS 101-01 Spring 2017 web page
  Algorithms and Abstract Data Types

CMPS 132/W Winter 2017 web page
  Computational Complexity and Computability

CMPS 101-02 Fall 2016 web page
  Algorithms and Abstract Data Types

Send email if you need to see: CMPS 101-02 Fall 2015 web page
  Algorithms and Abstract Data Types

Send email if you need to see: CMPS 101 Spring 2015 web page
  Algorithms and Abstract Data Types

CMPS 211 Winter 2015 web page
  Combinatorial Algorithms

CMPS 130 Fall 2014 web page
  Computational Models

CMPS 132 Spring 2014 web page
  Computational Complexity and Computability

CMPS 217 Winter 2014 web page
  Logic for Computer Science

Send email if you need to see: CMPS 101 Fall 2013 web page
  Algorithms and Abstract Data Types

Global Warming and Extreme Weather, A Quick Tutorial



Papers by Allen Van Gelder          Papers by Title         

Review-Period Papers by Title by Allen Van Gelder         

indexPapersPdf.html by Allen Van Gelder

Various software (ftp)

ColorSat misc files related to graph coloring with SAT

CarefulRanking documentation and code related to SAT 2011 paper.

ProofChecker documentation and code

WildBenches2009 has 20 benchmarks from the Application section of the SAT 2009 competition, phase 2.
The reason these are called wild is that their behavior seems to be rather unpredicatable. It might be that solver A solves instance 1 in a minute or so while solver B times out at 5 hours, and at the same time, solver B solves instance 2 in a minute or so while solver A times out at 5 hours. In some cases, slightly jiggling an instance or a parameter of the solver changes the time by a large factor. I am talking about good solvers that did well in this competition and/or earlier competitions.
The selection is heuristic, not scientific. My intention is to have a set of benchmarks that a researcher can conceivably solve completely without ANY timeouts. Some instances are SAT, some are UNSAT.
Also see the main web page http://www.satcompetition.org.

purse-poster.pdf SAT 2005 and 2007 Competition Scoring Rules
purse-poster.ps       and some 2005 results

JSAT System Description Papers
Call (unofficial)
Proposal and Motivation
Allen Van Gelder and Daniel LeBerre

CMPS201, Analysis of Algorithms, Fall 2009:
Fall 2009 web page

1ST CALL FOR WORKSHOPS, COMPETITIONS, AND TUTORIALS
Sixteenth International Conference on THEORY AND APPLICATIONS OF SATISFIABILITY TESTING --- SAT 2013

Also see the main web page http://sat2013.cs.helsinki.fi/.

sat2013-prefilled-lncs-copyright.pdf

Keywords for IJCAI 2013   as ASCII text file
IJCAI 2013 conference page



CMPS 201 Fall 2012 web page   Analysis of Algorithms




Information on Winter 2013 CMPS 132

Robots meta tag and robots.txt
According to https://support.google.com/webmasters/answer/6062596?hl=en&ref_topic=6061961
robots.txt must be at the root of the website host. We do not have privileges for that directory, so we should use meta tags on school computer systems to avoid search engines.
See https://developers.google.com/search/reference/robots_meta_tag

I think one puts the following in index.html in the "head" section to ask robots not to search the directory in which index.html resides. So do not put it in your primary web directory (PUBLIC_HTML usually). 

<meta name="robots" content="noindex" />


If you tell certain people the name of the directory, they will be able to visit it by typing it after the name of your public web directory.

As an experiment I made a "secret" directory named DoUSeeMeDir with some files in it besides index.html. You should be able to visit DoUSeeMeDir and view those files, but I hope the search engines do not show those files or even their names.

c-adt.ps c-adt.pdf

For information about Computer Algorithms, Third Edition by Sara Baase and myself, please click here to see Supplements (including errata, clarifications, sample code, javaToC hints)
or shift-click to download Supplements.tar (about 320 KB)
or visit these links to other servers, and use the Back button on your browser if you want to return to this page.
Prof. Baase's web site: http://www-rohan.sdsu.edu/faculty/baase
AWL Publisher's information
ISBN-13: 97802016124481612448
OBSOLETE Publisher's information
Prof. Ben Choi's web site at Louisiana Tech University for PowerPoint slides to accompany the text. He offered to make them available to other instructors.
http://www2.latech.edu/~choi/Bens/Teaching/Csc520/


Please click here to see TPTPparser (lex/yacc sources, linux/intel binary, sample input, README, tarball)


Please click here to see http://jsat.ewi.tudelft.nl (Journal of Satisfiability home page)


Information on dbx for C programs on Solaris machines

student-dbx-guide Text file, basics of using dbx. See CASE 3 for why to use cc/dbx rather than gcc/gdb.
student.dbxrc Sample dbx startup file, text for Solaris, hopefully self-explanatory.


Please click here to see Poster directory with some examples of using latex to make a poster.


Please click here to see CRA Best Practices Memo on Tenure Review (1999)

My Erdös number is 3, e.g. through the path AVG - Jeff Ullman - Ron Graham - PE. Also, my Erdös number of the second kind (where only two-authored papers count) is (at most) 7, through the path AVG - Jeff Ullman - John Hopcroft - Robert Tarjan - Andrew Yao - Nick Pippenger - Joel Spencer - PE. Thanks to Jan Johannsen for publicizing how to figure this out. Don't miss other interesting stuff on his home page, such as the Proof Complexity Theme Song.

SAT 2013

               Sixteenth International Conference on
        THEORY AND APPLICATIONS OF SATISFIABILITY TESTING
                        --- SAT 2013 ---

               Helsinki, Finland, July 8-12, 2013

Conference Web Page: http://sat2013.cs.helsinki.fi/

What Happened on Mars?

Visit this page of Raj Rajkumar to find out: http://users.ece.cmu.edu/~raj/mars.html

Read the story of how a priority inversion problem in the onboard software of the Mars Pathfinder was diagnosed and solved while Pathfinder was on Mars.

Personality_rights.txt