@misc(sksmodel,
 title        = {Skipping Simulation Model},
 url          = {http://www.ccs.neu.edu/home/jmitesh/sks},
)
@inproceedings(abadi1991existence,
 author       = {Mart{\'{\i}}n Abadi and Leslie Lamport},
 title        = {The Existence of Refinement Mappings},
 booktitle    = {Theoretical Computer Science, 1991},
 url          = {http://dx.doi.org/10.1016/0304-3975(91)90224-P},
)
@inproceedings(apt1986countable,
 author       = {Krzysztof R Apt and Gordon D Plotkin},
 title        = {Countable nondeterminism and random assignment},
 url          = {http://dx.doi.org/10.1145/6490.6494},
)
@inproceedings(barrett2005tvoc,
 author       = {Clark W. Barrett and Yi Fang and Benjamin Goldberg and Ying Hu and Amir Pnueli and Lenore D. Zuck},
 title        = {{TVOC:} {A} Translation Validator for Optimizing Compilers},
 booktitle    = {CAV, 2005},
 url          = {http://dx.doi.org/10.1007/11513988\_29},
)
@inproceedings(browne1988characterizing,
 author       = {Michael C. Browne and Edmund M. Clarke and Orna Grumberg},
 title        = {Characterizing Finite Kripke Structures in Propositional Temporal Logic},
 booktitle    = {Theoretical Computer Science, 1988},
 url          = {http://dx.doi.org/10.1016/0304-3975(88)90098-9},
)
@inproceedings(defdata,
 author       = {Harsh Raju Chamarthi and Peter C. Dillinger and Panagiotis Manolios},
 title        = {Data Definitions in the {ACL2} Sedan},
 booktitle    = {{ACL2} 2014},
 url          = {http://dx.doi.org/10.4204/EPTCS.152.3},
)
@inproceedings(acl2s11,
 author       = {Harsh Raju Chamarthi and Peter C. Dillinger and Panagiotis Manolios and Daron Vroon},
 title        = {The {ACL2} Sedan Theorem Proving System},
 booktitle    = {{TACAS} 2011},
 url          = {http://dx.doi.org/10.1007/978-3-642-19835-9\_27},
)
@inproceedings(van1990linear,
 author       = {Rob J. van Glabbeek},
 title        = {The Linear Time-Branching Time Spectrum (Extended Abstract)},
 booktitle    = {{CONCUR} 1990},
 url          = {http://dx.doi.org/10.1007/BFb0039066},
)
@inproceedings(hardin2001real,
 author       = {David S Hardin},
 title        = {Real-time objects on the bare metal: an efficient hardware realization of the Java TM Virtual Machine},
 booktitle    = {ISORC, 2001},
 doi          = {10.1109/ISORC.2001.922817},
)
@inproceedings(manolios2015sks,
 author       = {Mitesh Jain and Panagiotis Manolios},
 title        = {Skipping Refinement},
 booktitle    = {CAV, 2015},
 url          = {http://dx.doi.org/10.1007/978-3-319-21690-4\_7},
)
@inproceedings(larsen2000exploiting,
 author       = {Samuel Larsen and Saman P. Amarasinghe},
 title        = {Exploiting superword level parallelism with multimedia instruction sets},
 booktitle    = {PLDI, 2000},
 url          = {http://doi.acm.org/10.1145/349299.349320},
)
@phdthesis(manolios2001mechanical,
 author       = {P. Manolios},
 title        = {Mechanical verification of reactive systems},
 school       = {University of Texas},
)
@inproceedings(manolios2003compositional,
 author       = {Panagiotis Manolios},
 title        = {A Compositional Theory of Refinement for Branching Time},
 booktitle    = {{CHARME} 2003},
 url          = {http://dx.doi.org/10.1007/978-3-540-39724-3\_28},
)
@inproceedings(manolios2000correctness,
 author       = {Panagiotis Manolios},
 title        = {Correctness of Pipelined Machines},
 booktitle    = {{FMCAD}, 2000},
 url          = {http://dx.doi.org/10.1007/3-540-40922-X\_11},
)
@inproceedings(manolios2005computationally,
 author       = {Panagiotis Manolios and Sudarshan K. Srinivasan},
 title        = {A computationally effecient method based on commitment refinement maps for verifying pipelined machines},
 booktitle    = {MEMOCODE, 2005},
 url          = {http://dx.doi.org/10.1109/MEMCOD.2005.1487914},
)
@inproceedings(ray2004deductive,
 author       = {Sandip Ray and Warren A. Hunt Jr.},
 title        = {Deductive Verification of Pipelined Machines Using First-Order Quantification},
 booktitle    = {{CAV} 2004},
 url          = {http://dx.doi.org/10.1007/978-3-540-27813-9\_3},
)
@inproceedings(ray2013specification,
 author       = {Sandip Ray and Rob Sumners},
 title        = {Specification and Verification of Concurrent Programs Through Refinements},
 booktitle    = {Journal of Automated Reasoning},
 url          = {http://dx.doi.org/10.1007/s10817-012-9258-1},
)
@inproceedings(swords2010verified,
 author       = {Anna Slobodov{\'{a}} and Jared Davis and Sol Swords and Warren A. Hunt Jr.},
 title        = {A flexible formal verification framework for industrial scale validation},
 booktitle    = {{MEMOCODE}, 2011},
 url          = {http://dx.doi.org/10.1109/MEMCOD.2011.5970515},
)