nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

01.02.2014 | Introduction

Verification and validation meet planning and scheduling

verfasst von: Saddek Bensalem, Klaus Havelund, Andrea Orlandini

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 1/2014

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

A planning and scheduling (P&S) system takes as input a domain model and a goal, and produces a plan of actions to be executed, which will achieve the goal. A P&S system typically also offers plan execution and monitoring engines. Due to the non-deterministic nature of planning problems, it is a challenge to construct correct and reliable P&S systems, including, for example, declarative domain models. Verification and validation (V&V) techniques have been applied to address these issues. Furthermore, V&V systems have been applied to actually perform planning, and conversely, P&S systems have been applied to perform V&V of more traditional software. This article overviews some of the literature on the fruitful interaction between V&V and P&S.

Nächster Artikel A loop acceleration technique to speed up verification of automatically generated plans

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

In 2004 Remote Agent P&S scientist Kanna Rajan suggested to V&V scientist Klaus Havelund (both at NASA Ames Research Center at the time) to organize a workshop on the topic: “V&V of P&S systems”. The series was started in 2005 [2] and continued in 2009 [3] and 2011 [4].

Mars Science Laboratory (MSL) mission website. http://mars.jpl.nasa.gov/msl. Accessed Nov 2013

VVPS 2005 workshop website. http://icaps05.uni-ulm.de/workshops.html

VVPS 2009 workshop website. http://www-vvps09.imag.fr

VVPS 2011 workshop website. http://icaps11.icaps-conference.org/workshops/vvps.html

Abdedaim, Y., Asarin, E., Gallien, M., Ingrand, F., Lesire, C., Sighireanu, M.: Planning robust temporal plans: a comparison between CBTP and TGA approaches. In: Proceedings of the Seventeenth International Conference on Automated Planning and Scheduling (ICAPS’07), pp. 2–10 (2007)

Albarghouthi, A., Baier, J.A., McIlraith, S.A.: On the use of planning technology for verification. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test-case generation and runtime verification. Theor. Comput. Sci. 336(2–3), 209–234 (2005)CrossRefMATHMathSciNet

Artho, C., Havelund, K., Biere. A.: High-level data races. Softw. Test. Verif. Reliab. 13(4), 207–227 (2004)

Bakera, M., Edelkamp, S., Kissmann, P., Renner, C.D.: Solving \(\mu \)-calculus parity games by symbolic planning. In: Peled. D., Wooldridge, M. (eds.) MoChArt. Lecture Notes in Computer Science, vol. 5348, pp. 15–33. Springer, New York (2008)

10.

Barringer, H., Groce, A., Havelund, K., Smith, M.: Formal analysis of log files. J. Aerosp. Comput. Inf. Commun. 7(11), 365–390 (2010)CrossRef

11.

Barringer, H., Havelund, K., Kurklu, E., Morris, R.: Checking flight rules with TraceContract: application of a Scala DSL for trace analysis. In: Scala Days 2011. Stanford University, California (2011)

12.

Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K., Lime, D.: UPPAAL-TIGA: time for playing games! In: Proceedings of 19th International Conference on Computer Aided Verification (CAV’07), vol. 4590 in LNCS, pp. 121–125. Springer, New York (2007)

13.

Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J.: Efficient Guiding Towards Cost-Optimality in UPPAAL. Springer, New York (2001)

14.

Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS’05) (2005)

15.

Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing conformance of real-time applications: case of planetary rover controller. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS’05), pp. 23–32 (2005)

16.

Bodik, R., Jobstmann, B.: Algorithmic program synthesis: introduction. Int. J. Softw. Tools Technol. Transf. STTT 15(5–6), 397–411 (October 2013)

17.

Bozzano, M., Cimatti, A., Roveri, M., Tchaltsev, A.: A comprehensive approach to on-board autonomy verification and validation. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

18.

Brat, G., Drusinsky, D., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Visser, W., Washington, R.: Experimental evaluation of verification and validation tools on Martian rover software. Form. Methods Syst. Des. 25(2), 167–198 (2004)

19.

Brat, G., Gannakopoulou, D., Izygon, M., Alex, E., Wang, L., Frank, J., Molin, A.: Model-based verification and validation for procedure authoring. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

20.

Cerrito, S., Mayer, M.C.: Using linear temporal logic to model and solve planning problems. In: Giunchiglia, F (ed.) Artificial Intelligence: Methodology, Systems, and Applications. Lecture Notes in Computer Science, vol 1480, pp. 141–152. Springer, New York (1998)

21.

Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Verifying flexible timeline-based plans. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

22.

Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Flexible plan verification: feasibility results. Fundamenta Informaticae 107, 111–137 (2011)MATHMathSciNet

23.

Cichy, B., Chien, S., Schaffer, S., Tran, D., Rabideau, G., Sherwood, R.: Validating the autonomous EO-1 science agent. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS’05), pp. 75–85 (2005)

24.

Cimatti, A., Giunchiglia, F., Giunchiglia, E., Traverso, P.: Planning via model checking: a decision procedure for AR. In: Steel, S., Alami, R. (eds.) ECP. Lecture Notes in Computer Science, vol. 1348, pp. 130–142. Springer, New York (1997)

25.

Cimatti, A., Roveri, M., Traverso, P.: Strong planning in non-deterministic domains via model checking. In: Simmons, R.G., Veloso, M.M., Smith, S.F. (eds.) AIPS, pp. 36–43. AAAI, Pittsburgh (1998)

26.

Crampton, J., Huth, M., Kuo, J.H.-P.: Authorized workflow schemas : deciding realizability through LTL(F) model checking. Int. J. Softw. Tools Technol. Transf. STTT (2014)

27.

Dierks, H.: Finding optimal plans for domains with restricted continuous effects with UPPAAL-CORA. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS’05) (2005)

28.

Dixon, L., Smaill, A., Bundy, A.: Verified planning by deductive synthesis in intuitionistic linear logic. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

29.

Edelkamp, S.: Promela planning. In: Ball, T., Rajamani, S.K. (eds.) SPIN. Lecture Notes in Computer Science, vol. 2648, pp. 197–212. Springer, New York (2003)

30.

Edelkamp, S., Jabbar, S.: Action planning for directed model checking of Petri nets. Electr. Notes Theor. Comput. Sci. 149(2), 3–18 (2006)CrossRef

31.

Edelkamp, S., Jabbar, S., Lluch-Lafuente, A.: Cost-algebraic heuristic search. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 1362–1367. AAAI Press/The MIT Press, Cambridge (2005)

32.

Edelkamp, S., Kellershoff, M., Sulewski, D.: Program model checking via action planning. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt. Lecture Notes in Computer Science, vol. 6572, pp. 32–51. Springer, New York (2010)

33.

Feather, M., Smith, B.: Automatic generation of test oracles—from pilot studies to application. Autom. Softw. Eng. 8(1), 31–61 (2001)CrossRefMATH

34.

Fox, M., Howey, R., Long, D.: Exploration of the robustness of plans. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS’05), pp. 67–74 (2005)

35.

Fox, M., Long, D., Baldwin, L., Wilson, G., Woods, M., Jameux, D., Aylett, R.: On-board timeline validation and repair: a feasibility study. In: Proceedings of 5th International Workshop on Planning and Scheduling for Space (IWPSS’06) (2006)

36.

Freitag, B., Margaria, T., Steffen, B.: A pragmatic approach to software synthesis. In: Wing, J.M., Wexelblat, R.L. (eds.) Workshop on Interface Definition Languages, Portland, Oregon, USA, pp. 46–58. ACM Press, New York (1994)

37.

Giannakopoulou, D., Pasareanu, C.S., Lowry, M., Washington, R.: Lifecycle verification of the NASA Ames K9 rover executive. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS’05), pp. 75–85 (2005)

38.

Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) ECP. Lecture Notes in Computer Science, vol. 1809, pp. 1–20. Springer, New York (1999)

39.

Goldberg, A., Havelund, K., McGann, C.: Runtime verification for autonomous spacecraft software. In: Proceedings of IEEE Aerospace Conference, IEEE Computer Society, USA (2005)

40.

Goldman, R.P., Kuter, U., Schneider, A.: Using classical planners for plan verification and counterexample generation. In: Proceedings of AAAI Workshop on Problem Solving Using Classical, Planning (2012)

41.

Goldman, R.P., Musliner, D.J., Pelican, M.J.: Exploiting implicit representations in timed automaton verification for controller synthesis. In: Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control (HSCC’02) (2002)

42.

Goldman, R.P., Pelican, M.J., Musliner, D.J.: A loop acceleration technique to speed up verification of automatically-generated plans. Int. J. Softw. Tools Technol. Transf. STTT (2014)

43.

Havelund, K., Groce, A., Holzmann, G., Joshi, R., Smith, M.: Automated testing of planning models. In: Proceedings of the Fifth International Workshop on Model Checking and Artificial Intelligence, pp. 90–105 (2008)

44.

Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J.L.: Formal analysis of the Remote Agent—before and after flight. In: The Fifth NASA Langley Formal Methods Workshop, Virginia (2001)

45.

Havelund, K., Lowry, M., Penix, J.: Formal analysis of a spacecraft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749–765 (2001). An earlier version occurred in the proceedings of 4th SPIN, workshop, 1998CrossRef

46.

Howey, R., Long, D.: VAL’s progress: the automatic validation tool for PDDL2.1 used in the international planning competition. In: Proceedings of the ICAPS Workshop on The Competition: Impact, Organization, Evaluation, Benchmarks, pp. 28–37, Trento (2003)

47.

Johnston, M.D., Tran, D.: Verification and validation of a deep space network scheduling application. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

48.

Jonsson, A., Morris, P., Muscettola, N., Rajan, K., Smith, B.: Planning in interplanetary space: theory and practice. In: Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling (AIPS’00), pp. 177–186 (2000)

49.

Kautz, H., Selman, B.: BLACKBOX: a new approach to the application of theorem proving to problem solving. In: AIPS’98 Workshop on Planning as Combinatorial, Search, pp. 58–60 (1998)

50.

Kautz, H., Selman, B.: Unifying sat-based and graph-based planning. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI-99), vol. 99, pp. 318–325 (1999)

51.

Kautz, H.A., Selman, B., et al.: Planning as satisfiability. In: Proceedings of the International European Conference on Artificial Intelligence (ECAI-92), vol. 92, pp. 359–363 (1992)

52.

Khatib, L., Muscettola, N., Havelund, K.: Verification of plan models using UPPAAL. In: First International Workshop on Formal Approaches to Agent-Based Systems, NASA’s Goddard Space center, Maryland. Lecture Notes in Artificial Intelligence, vol. 1871. Springer, New York (2000)

53.

Khatib, L., Muscettola, N., Havelund, K.: Mapping temporal planning constraints into timed automata. In: The Eigth International Symposium on Temporal Representation and Reasoning (TIME’01), pp. 21–27 (2001)

54.

Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS’05), Pittsburgh, pp. 531–542 (2005)

55.

Lindsey, T., Pecheur, C.: Simulation-based verification of autonomous controllers with Livingstone PathFinder. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04), Barcelona, Spain. Lecture Notes in Computer Science, vol. 2988 (2004)

56.

Long, D., Fox, M., Howey, R.: Planning domains and plans: validation, verification and analysis. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

57.

Lowry, M.R., Havelund, K., Penix, J.: Verification and validation of AI systems that control deep-space spacecraft. In: Foundations of Intelligent Systems, Proceedings of 10th International Symposium, ISMIS’97, Charlotte. Lecture Notes in Computer Science, vol. 1325, pp. 35–47. Springer, New York (1997)

58.

Mayer, M.C., Limongelli, C., Orlandini, A., Poggioni, V.: Linear temporal logic as an executable semantics for planning languages. J. Log. Lang. Inf. 16(1), 63–89 (2007)CrossRefMATHMathSciNet

59.

McCarthy, J., Hayes, P.: Some Philosophical Problems from the Standpoint of Artificial Intelligence. Stanford University, USA (1968)

60.

McDermott, D., Ghallab, M., Howe, A., Knoblock, C., Ram, A., Veloso, M., Weld, D., Wilkins, D.: PDDL-the planning domain definition language. Technical Report CVC TR98003/DCS TR1165, New Haven, CT. Yale Center for Computational Vision and Control (1998)

61.

Menzies, T., Pecheur, C.: Verification and validation and artificial intelligence. Adv. Comput. 65, 5–45 (2005)

62.

Morris, P.H., Muscettola, N.: Temporal dynamic controllability revisited. In: Proceedings of the 20th National Conference on Artificial Intelligence (AAAI-05) (2005)

63.

Muscettola, N.: HSTS: integrating planning and scheduling. In: Zweben, M., Fox, M.S. (eds.) Intelligent Scheduling. Morgan Kauffmann, Burlington (1994)

64.

Musliner, D.J., Pelican, M.J.S., Schlette, P.J.: Verifying equivalence of procedures in different languages: preliminary results. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

65.

Nayak, P.P., Bernard, D.E., Dorais, G., Gamble, E.B., Kanefsky, B., Kurien, J., Millar, W., Muscettola, N., Rajan, K., Rouquette, N., Smith, B.D., Taylor, W.: Validating the DS1 Remote Agent experiment. In: Proceeedings of the Fifth International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS’99) (1999)

66.

Orlandini, A., Finzi, A., Cesta, A., Fratini, S.: TGA-based controllers for flexible plan execution. In: Advances in Artificial Intelligence (KI 2011), 34th Annual German Conference on AI. Lecture Notes in Computer Science, vol. 7006, pp. 233–245. Springer, New York (2011)

67.

Patron, P., Birch, A.: Plan proximity: an enhanced metric for plan stability. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

68.

Penix, J., Pecheur, C., Havelund, K.: Using model checking to validate AI planner domain models. In: Proceedings of the 23\(^{rd}\) Annual Software Engineering, Workshop (1998)

69.

Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’06). Lecture Notes in Computer Science, vol. 3855, pp. 364–380. Springer, New York (2006)

70.

Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE Computer Society, USA (1977)

71.

Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages (POPL’89), pp. 179–190 (1989)

72.

Preece, A.: Evaluating verification and validation methods in knowledge engineering. In: Roy, R. (ed.) Micro-Level Knowledge Management, pp. 123–145. Morgan-Kaufman, Burlington (2001)

73.

R-Moreno, M.D., Brat, G., Muscettola, N., Rijsman, D.: Validation of a multi-agent architecture for planning and execution. In: Proceedings of 18th International Workshop on Principles of Diagnosis (DX’07) (2007)

74.

Raimondi, F., Pecheur, C., Brat, G.: PDVer, a tool to verify PDDL planning domains. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

75.

Razavi, N., Farzan, A., McIlraith, S.A.: Generating effective tests for concurrent programs via AI automated planning techniques. Int. J. Softw. Tools Technol. Transf. STTT (2014)

76.

Shah, M., Chrpa, L., Jimoh, F., Kitchin, D., McCluskey, T., Parkinson, S., Vallati, M.: Knowledge engineering tools in planning: state-of-the-art and future challenges. In: Proceedings of the ICAPS Workshop on Knowledge Engineering for Planning and Scheduling (KEPS 2013) (2013)

77.

Siminiceanu, R.I., Butler, R.W., Munoz, C.A.: Experimental evaluation of a planning language suitable for formal verification. In: Proceedings of the Fifth International Workshop on Model Checking and Artificial Intelligence, pp. 18–34 (2008)

78.

Smith, B., Feather, M., Muscettola, N.: Challenges and methods in testing the Remote Agent planner. In: Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling (AIPS’00), pp. 254–263 (2000)

79.

Smith, B., Millar, W., Dunphy, J., Tung, Y.-W., Nayak, P., Gamble, E., Clark, M.: Validation and verification of the Remote Agent for spacecraft autonomy. In: Proceedings of IEEE Aerospace Conference (1999)

80.

Smith, B., Rajan, K., Muscettola, N.: Knowledge acquisition for the onboard planner of an autonomous spacecraft. In: 10th European Workshop on Knowledge Acquisition, Modeling and Management (EKAW’97). Lecture Notes in Computer Science, vol. 1319, pp. 253–268 (1997)

81.

Smith, M.H., Holzmann, G.J., Cucullu, G.C., Smith, B.D.: Model checking autonomous planners: even the best laid plans must be verified. In: Proceedings of IEEE Aerospace Conference, pp. 1–11. IEEE Computer Society, USA (2005)

82.

Srivastava, S., Immerman, N., Zilberstein, S.: Finding plans with branches, loops and preconditions. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS’09) (2009)

83.

Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation. In: Bartocci, E., Ramakrishnan, C. (eds.) Model Checking Software, vol. 7976, pp. 341–357. Lecture Notes in Computer Science. Springer, Berlin (2013)

84.

Steffen, B., Margaria, T., Braun, V.: The electronic tool integration platform: concepts and design. Int. J. Softw. Tools Technol. Transf. STTT 1(1–2), 9–30 (1997)CrossRefMATH

85.

Vaquero, T., Silva, J., Beck, J.: A brief review of tools and methods for knowledge engineering for planning and scheduling. In: Proceedings of the ICAPS Workshop on Knowledge Engineering for Planning and Scheduling (KEPS 2011) (2011)

86.

Vidal, T.: A unified dynamic approach for dealing with temporal uncertainty and conditional planning. In: Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling (AIPS’00) (2000)

87.

Wehrle, M. Helmert, M.: The causal graph revisited for directed model checking. In: Palsberg, J., Su, Z. (eds.) SAS. Lecture Notes in Computer Science, vol. 5673, pp. 86–101. Springer, New York (2009)

88.

Williams, B.C., Nayak, P.P.: A model-based approach to reactive self-configuring systems. AAAI/IAAI 2, 971–978 (1996)

Titel: Verification and validation meet planning and scheduling
verfasst von: Saddek Bensalem
Klaus Havelund
Andrea Orlandini
Publikationsdatum: 01.02.2014
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 1/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-013-0294-x

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 1/2014

Symbolic object code analysis

A loop acceleration technique to speed up verification of automatically generated plans

Generating effective tests for concurrent programs via AI automated planning techniques

Constraint-based BMC: a backjumping strategy

Authorized workflow schemas: deciding realizability through model checking

Open source software-defined radio tools for education, research, and rapid prototyping