+publisher:"Worcester Polytechnic Institute" +contributor:("Daniel J. Dougherty, Advisor")

1. VanValkenburg, MaryAnn E. Alloy-Guided Verification of Cooperative Autonomous Driving Behavior.

Degree: MS, 2020, Worcester Polytechnic Institute

URL: etd-3956 ; https://digitalcommons.wpi.edu/etd-theses/1354

► Alloy is a lightweight formal modeling tool that generates instances of a software specification to check properties of the design. This work demonstrates the… (more)

Subjects/Keywords: Alloy; Formal modeling; Cooperative autonomous driving (CAD); Formal verification

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

VanValkenburg, M. E. (2020). Alloy-Guided Verification of Cooperative Autonomous Driving Behavior. (Thesis). Worcester Polytechnic Institute. Retrieved from etd-3956 ; https://digitalcommons.wpi.edu/etd-theses/1354

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

VanValkenburg, MaryAnn E. “Alloy-Guided Verification of Cooperative Autonomous Driving Behavior.” 2020. Thesis, Worcester Polytechnic Institute. Accessed January 18, 2021. etd-3956 ; https://digitalcommons.wpi.edu/etd-theses/1354.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

VanValkenburg, MaryAnn E. “Alloy-Guided Verification of Cooperative Autonomous Driving Behavior.” 2020. Web. 18 Jan 2021.

Vancouver:

VanValkenburg ME. Alloy-Guided Verification of Cooperative Autonomous Driving Behavior. [Internet] [Thesis]. Worcester Polytechnic Institute; 2020. [cited 2021 Jan 18]. Available from: etd-3956 ; https://digitalcommons.wpi.edu/etd-theses/1354.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

VanValkenburg ME. Alloy-Guided Verification of Cooperative Autonomous Driving Behavior. [Thesis]. Worcester Polytechnic Institute; 2020. Available from: etd-3956 ; https://digitalcommons.wpi.edu/etd-theses/1354

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

2. Giannakopoulos, Theophilos John. Multi-Decision Policy and Policy Combinator Specifications.

Degree: MS, 2012, Worcester Polytechnic Institute

URL: etd-022112-163738 ; https://digitalcommons.wpi.edu/etd-theses/166

► Margrave is a specification language and analysis tool for access control policies with semantics based in order-sorted logic. The clear logical roots of Margrave's… (more)

Subjects/Keywords: formal methods; access control; policy combinators; policies; specifications; Margrave

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Giannakopoulos, T. J. (2012). Multi-Decision Policy and Policy Combinator Specifications. (Thesis). Worcester Polytechnic Institute. Retrieved from etd-022112-163738 ; https://digitalcommons.wpi.edu/etd-theses/166

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Giannakopoulos, Theophilos John. “Multi-Decision Policy and Policy Combinator Specifications.” 2012. Thesis, Worcester Polytechnic Institute. Accessed January 18, 2021. etd-022112-163738 ; https://digitalcommons.wpi.edu/etd-theses/166.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Giannakopoulos, Theophilos John. “Multi-Decision Policy and Policy Combinator Specifications.” 2012. Web. 18 Jan 2021.

Vancouver:

Giannakopoulos TJ. Multi-Decision Policy and Policy Combinator Specifications. [Internet] [Thesis]. Worcester Polytechnic Institute; 2012. [cited 2021 Jan 18]. Available from: etd-022112-163738 ; https://digitalcommons.wpi.edu/etd-theses/166.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Giannakopoulos TJ. Multi-Decision Policy and Policy Combinator Specifications. [Thesis]. Worcester Polytechnic Institute; 2012. Available from: etd-022112-163738 ; https://digitalcommons.wpi.edu/etd-theses/166

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

3. Nelson, Tim. First-Order Models for Configuration Analysis.

Degree: PhD, 2013, Worcester Polytechnic Institute

URL: etd-042513-142414 ; https://digitalcommons.wpi.edu/etd-dissertations/452

► Our world teems with networked devices. Their configuration exerts an ever-expanding influence on our daily lives. Yet correctly configuring systems, networks, and access-control policies… (more)

▼ Our world teems with networked devices. Their configuration exerts an ever-expanding influence on our daily lives. Yet correctly configuring systems, networks, and access-control policies is notoriously difficult, even for trained professionals. Automated static analysis techniques provide a way to both verify a configuration's correctness and explore its implications. One such approach is scenario-finding: showing concrete scenarios that illustrate potential (mis-)behavior. Scenarios even have a benefit to users without technical expertise, as concrete examples can both trigger and improve users' intuition about their system. This thesis describes a concerted research effort toward improving scenario-finding tools for configuration analysis. We developed Margrave, a scenario-finding tool with special features designed for security policies and configurations. Margrave is not tied to any one specific policy language; rather, it provides an intermediate input language as expressive as first-order logic. This flexibility allows Margrave to reason about many different types of policy. We show Margrave in action on Cisco IOS, a common language for configuring firewalls, demonstrating that scenario-finding with Margrave is useful for debugging and validating real-world configurations. This thesis also presents a theorem showing that, for a restricted subclass of first-order logic, if a sentence is satisfiable then there must exist a satisfying scenario no larger than a computable bound. For such sentences scenario-finding is complete: one can be certain that no scenarios are missed by the analysis, provided that one checks up to the computed bound. We demonstrate that many common configurations fall into this subclass and give algorithmic tests for both sentence membership and counting. We have implemented both in Margrave. Aluminum is a tool that eliminates superfluous information in scenarios and allows users' goals to guide which scenarios are displayed. We quantitatively show that our methods of scenario-reduction and exploration are effective and quite efficient in practice. Our work on Aluminum is making its way into other scenario-finding tools. Finally, we describe FlowLog, a language for network programming that we created with analysis in mind. We show that FlowLog can express many common network programs, yet demonstrate that automated analysis and bug-finding for FlowLog are both feasible as well as complete. Advisors/Committee Members: Shriram Krishnamurthi, Committee Member, Joshua D. Guttman, Committee Member, Daniel J. Dougherty, Advisor, Kathi Fisler, Advisor, Craig E. Wills, Department Head.

Subjects/Keywords: static analysis; model finding; security; firewalls; configuration; scenarios; logic

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Nelson, T. (2013). First-Order Models for Configuration Analysis. (Doctoral Dissertation). Worcester Polytechnic Institute. Retrieved from etd-042513-142414 ; https://digitalcommons.wpi.edu/etd-dissertations/452

Chicago Manual of Style (16^th Edition):

Nelson, Tim. “First-Order Models for Configuration Analysis.” 2013. Doctoral Dissertation, Worcester Polytechnic Institute. Accessed January 18, 2021. etd-042513-142414 ; https://digitalcommons.wpi.edu/etd-dissertations/452.

MLA Handbook (7^th Edition):

Nelson, Tim. “First-Order Models for Configuration Analysis.” 2013. Web. 18 Jan 2021.

Vancouver:

Nelson T. First-Order Models for Configuration Analysis. [Internet] [Doctoral dissertation]. Worcester Polytechnic Institute; 2013. [cited 2021 Jan 18]. Available from: etd-042513-142414 ; https://digitalcommons.wpi.edu/etd-dissertations/452.

Council of Science Editors:

Nelson T. First-Order Models for Configuration Analysis. [Doctoral Dissertation]. Worcester Polytechnic Institute; 2013. Available from: etd-042513-142414 ; https://digitalcommons.wpi.edu/etd-dissertations/452

4. Saghafi, Salman. A Framework for Exploring Finite Models.

Degree: PhD, 2015, Worcester Polytechnic Institute

URL: etd-043015-110044 ; https://digitalcommons.wpi.edu/etd-dissertations/458

► This thesis presents a framework for understanding first-order theories by investigating their models. A common application is to help users, who are not necessarily… (more)

Subjects/Keywords: exploration; finite model-finding; first-order logic; provenance information; Chase; Geometric Logic; Razor; Aluminum

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Saghafi, S. (2015). A Framework for Exploring Finite Models. (Doctoral Dissertation). Worcester Polytechnic Institute. Retrieved from etd-043015-110044 ; https://digitalcommons.wpi.edu/etd-dissertations/458

Chicago Manual of Style (16^th Edition):

Saghafi, Salman. “A Framework for Exploring Finite Models.” 2015. Doctoral Dissertation, Worcester Polytechnic Institute. Accessed January 18, 2021. etd-043015-110044 ; https://digitalcommons.wpi.edu/etd-dissertations/458.

MLA Handbook (7^th Edition):

Saghafi, Salman. “A Framework for Exploring Finite Models.” 2015. Web. 18 Jan 2021.

Vancouver:

Saghafi S. A Framework for Exploring Finite Models. [Internet] [Doctoral dissertation]. Worcester Polytechnic Institute; 2015. [cited 2021 Jan 18]. Available from: etd-043015-110044 ; https://digitalcommons.wpi.edu/etd-dissertations/458.

Council of Science Editors:

Saghafi S. A Framework for Exploring Finite Models. [Doctoral Dissertation]. Worcester Polytechnic Institute; 2015. Available from: etd-043015-110044 ; https://digitalcommons.wpi.edu/etd-dissertations/458

5. Adler, Jonathan D. Graph Decompositions and Monadic Second Order Logic.

Degree: MS, 2009, Worcester Polytechnic Institute

URL: etd-042709-164059 ; https://digitalcommons.wpi.edu/etd-theses/364

► A tree decomposition is a tool which allows for analysis of the underlying tree structure of graphs which are not trees. Given a class… (more)

Subjects/Keywords: clique width; tree decompositions; logic; graph theory

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Adler, J. D. (2009). Graph Decompositions and Monadic Second Order Logic. (Thesis). Worcester Polytechnic Institute. Retrieved from etd-042709-164059 ; https://digitalcommons.wpi.edu/etd-theses/364

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Adler, Jonathan D. “Graph Decompositions and Monadic Second Order Logic.” 2009. Thesis, Worcester Polytechnic Institute. Accessed January 18, 2021. etd-042709-164059 ; https://digitalcommons.wpi.edu/etd-theses/364.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Adler, Jonathan D. “Graph Decompositions and Monadic Second Order Logic.” 2009. Web. 18 Jan 2021.

Vancouver:

Adler JD. Graph Decompositions and Monadic Second Order Logic. [Internet] [Thesis]. Worcester Polytechnic Institute; 2009. [cited 2021 Jan 18]. Available from: etd-042709-164059 ; https://digitalcommons.wpi.edu/etd-theses/364.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Adler JD. Graph Decompositions and Monadic Second Order Logic. [Thesis]. Worcester Polytechnic Institute; 2009. Available from: etd-042709-164059 ; https://digitalcommons.wpi.edu/etd-theses/364

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

		in
And / Or
		in
And / Or
		in
And / Or
		in

Open Access Theses and Dissertations