gl-term-level/paper.bib at master · solswords/gl-term-level · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
@misc{acl2:home,
 author       = "{Matt Kaufmann and J S. Moore}",
 title        = "{ACL2} home page",
 key        = "{ACL2} home page",
 note         = "(see URL \url{http://www.cs.utexas.edu/users/moore/acl2})",
 year       = "Accessed: 2016"
}

@inproceedings{bit-blasting-GL,
  author    = "{Sol Swords and Jared Davis}",
  title     = "{Bit-Blasting {ACL2} Theorems}",
  booktitle = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover
               and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4,
               2011.},
  pages     = {84--102},
  year      = {2011},
  url       = {http://dx.doi.org/10.4204/EPTCS.70.7},
  doi       = {10.4204/EPTCS.70.7},
  timestamp = {Mon, 28 Oct 2013 16:56:55 +0100},
}

@PhdThesis{gl-diss,
  author  = "{Sol Swords}",
  title   = "{A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover}",
  school  = "{Department of Computer Sciences,
             The University of Texas at Austin}",
  year    = "2010",
  url={http://repositories.lib.utexas.edu/handle/2152/ETD-UT-2010-12-2210}
}


@inproceedings{kaufmann2002efficient,
  title={Efficient rewriting of operations on finite structures in ACL2},
  author={Kaufmann, Matt and Sumners, Rob},
  booktitle={Proceedings of the 3rd International Workshop on the {ACL2} Theorem Prover
               and its Applications},
  pages={141--150},
  year={2002}
}

@misc{acl2:doc,
 author       = "{ACL2 Community}",
 title        = "{ACL2+Books} Documentation",
 key        = "{ACL2+Books} Documentation",
 note         = "See URL \url{http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html?topic=ACL2____ACL2}",
year = "accessed January, 2017"
}

@inproceedings{davis2014microcode,
  title={Microcode Verification--Another Piece of the Microprocessor Verification Puzzle},
  author={Davis, Jared and Slobodova, Anna and Swords, Sol},
  booktitle={International Conference on Interactive Theorem Proving},
  pages={1--16},
  year={2014},
  organization={Springer}
}


@inproceedings{hardinucode,
  title={A robust machine code proof framework for highly secure applications},
  author={Hardin, David S and Smith, Eric W and Young, William D},
  booktitle={Proceedings of the Sixth International Workshop on the {ACL2} Theorem Prover and its Applications},
  pages={11--20},
  year={2006},
  url  = {http://dl.acm.org},
  organization={ACM}
}

@Inproceedings{fixyourtypes,
  author    = {Swords, Sol and Davis, Jared},
  year      = {2015},
  title     = {Fix Your Types},
  editor    = {Kaufmann, Matt and Rager, David L.},
  booktitle = {{\rm Proceedings Thirteenth International Workshop on the}
               ACL2 Theorem Prover and Its Applications,
               {\rm Austin, Texas, USA, 1-2 October 2015}},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {192},
  publisher = {Open Publishing Association},
  pages     = {3-16},
  doi       = {10.4204/EPTCS.192.2},
}