= Welcome to GMC = 

== Multi-Core Model Checking ==

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


'''edu.udel.cis.vsl.civl.kripke.common.CommonEvaluator.java'''[[BR]]

boundVariableStack [[BR]]

originalState [[BR]]

originalPid [[BR]]

valueAtOrRemoteCount [[BR]]

''Possible solution'': spawn an EvaluatorWorker[[BR]]


'''edu.udel.cis.vsl.civl.semantics.common.CommonExecutor.java'''[[BR]]

numSteps[[BR]]

''Possible solution'': Each thread has its own copy of Executor.[[BR]]