= Welcome to GMC = 

== Multi-Core Model Checking ==

Stateful classes in CIVL that may not be necessary to be stateful:

'''edu.udel.cis.vsl.civl.kripke.common.CommonEvaluator.java'''
boundVariableStack 
originalState 
originalPid 
valueAtOrRemoteCount 
''Possible solution'': spawn an EvaluatorWorker

'''edu.udel.cis.vsl.civl.semantics.common.CommonExecutor.java'''
numSteps
''Possible solution'': Each thread has its own copy of Executor.