John V Franco
Professional Summary
Prof. Franco is director of the National Center of Academic Excellence in Cyber Operations at the University of Cincinnati. The Center is a collaborative effort involving three university colleges, and two local major defense contractors for advanced training in cyber operations and cyber security.
Prof. Franco is editor-in-chief of the Journal on Satisfiability, Boolean Modeling, and Computation, and an editor of the Annals of Mathematics and Artificial Intelligence. He is Vice Chair of the SAT Association and a member of the steering committee for the annual Internation Conference on the Theory and Applications of Satisfiability Testing.
Prof. Franco has been PI, Co-PI, or Senior Personnel on 18 grants and contracts from the ONR, AFOSR, EPA, NSA, and NSF. He spent 9 months sabbatical leave at Fort George G. Meade in Research and Engineering on Satisfiability research, was visiting scientist at FAW, Ulm, Germany for three summers, and visiting scientist at U. Paderborn for a summer.
Education
Ph.D in Computer Science: Rutgers the State University of New Jersey 1981 (Computer Science)
M.S. in E.E.: Columbia University New York, 1971 (Electrical Engineering)
B.S. in E.E.: City College of New York New York City, 1969 (Electrical Engineering)
Research and Practice Interests
Information assurance, cyber defense, design & analysis of SAT algorithms, applications of SAT to network and computer security, formal methods, model checking, interactive first order logic theorem provers.
Research Support
Grant: #MDA90402C1162/P00005 Investigators:Franco, John 03-27-2002 -08-31-2004 National Security Agency Satisfiability Algorithm Research and Development to Enhance Formal Verification Tools Role:PI $561,906.00 Closed Level:Federal
Grant: #MDA90499C4547/P00004 Investigators:Franco, John 06-22-1999 -09-30-2001 National Security Agency Satisfiability Algorithm Research and Development to Enhance Formal Verification Tools Role:PI $493,185.00 Closed Level:Federal
Investigators:Franco, John 11-01-1998 -10-31-1999 Advanced Computing Systems Association Perl to JVM Optimization Role:PI $21,269.00 Closed Level:Private Non-Profit
Grant: #SRS 006291 Investigators:Franco, John 07-06-2009 -03-31-2010 National Security Agency Integrated Algebraic and Resolution Algorithms for Improved Solutions to Difficult Problems Role:PI $61,549.00 Closed Level:Federal
Grant: #DUE-1244697 Investigators:Bhattacharya, Prabir; Franco, John 09-15-2013 -08-31-2016 National Science Foundation Collaborative Research: Real World Relevant Security Labware for Mobile Analysis and Protection Experience Role:Collaborator $140,002.00 Awarded Level:Federal
Grant: #EEC-1404766 Investigators:Angelopoulos, Anastasios; Bhattacharya, Prabir; Cohen, Kelly; Franco, John; Guliants, Vadim; Kastner, Jeffrey; Kukreti, Anant; Kupferle, Margaret; Lu, Mingming; Nistor, Vasille; Sorial, George; Wei, Heng; Wendell, David 05-01-2014 -04-30-2017 National Science Foundation RET Site on "Challenge-Based Learning and Engineering Design Process Enhanced Research Experiences for Middle and High School In-Service Teachers." Role:Collaborator $498,949.00 Awarded Level:Federal
Grant: #0416-CS-PB-UC / NSF 1636995 Investigators:Franco, John 04-01-2016 -08-31-2017 National Science Foundation Real World Relevant Security Labware for Mobile Threat Analysis and Protection Experience Role:PI $21,300.00 Active Level:Federal
Grant: #H98230-17-1-0345 Investigators:Franco, John; Li, Chengcheng 07-01-2017 -06-30-2018 National Security Agency Train and Certify Qualified Instructors to Teach CAE's Cybersecurity Curricula Role:Collaborator $497,782.06 Awarded Level:Federal
Grant: #ODHE Cyber Range Investigators:Baker, Vicki; Cahay, Marc; Franco, John; Gerst, Jason; Harknett, Richard; Li, Chengcheng; Said, Hazem; Verkamp, Brian 07-01-2017 -06-30-2019 Ohio Department of Higher Education Ohio Cyber Range Role:Collaborator $1,900,000.00 Active Level:State of Ohio
Grant: #ODHE RAPIDS 2018 Investigators:Atluri, Gowtham; Franco, John; Li, Chengcheng 07-01-2017 -06-30-2018 Ohio Department of Higher Education RAPIDS Equipment Request Role:PI $253,395.00 Active Level:State of Ohio
Grant: #H98230-18-1-0333 Investigators:Franco, John 09-05-2018 -09-04-2019 National Security Agency 12.905 CAE-CO 2018/2019 Curriculum Development Initiatives Role:PI $59,999.97 Active Level:Federal
Grant: #H98230-19-1-0297 Investigators:Franco, John; Niu, Nan 09-01-2019 -08-31-2020 National Security Agency Automated detection and resolution of software vulnerabilities in critical and dependable systems where hundreds and thousands of features interact with each other in complex and subtle manners. Role:PI $92,193.00 Awarded Level:Federal
Grant: #Riverside Research Institute DRC.11373.RR001834.20 sub WSARC sub OFRN Investigators:Franco, John 03-01-2020 -08-31-2021 Wright State Applied Research Corporation Computer-Human Interaction for Rapid Program Analysis through Cognitive Collaboration (CHIRP2C) Role:PI $100,000.00 Awarded Level:Private Non-Profit
Grant: #H98230-20-1-0365 Investigators:Franco, John; Niu, Nan 09-10-2020 -12-30-2021 National Security Agency Automated detection and resolution of software vulnerabilities in critical and dependable systems where hundreds and thousands of features interact with each other in complex and subtle manners. Role:PI $72,392.00 Awarded Level:Federal
Grant: #H98230-21-1-0315 Investigators:Franco, John; Niu, Nan 08-23-2021 -12-31-2022 National Security Agency Automated Reverse Engineering Tools and Detection and Resolution of Software vulnerabilities in Critical and Dependable Systems Role:PI 72431.00 Awarded Level:Federal
Publications
Peer Reviewed Publications
J Gu, PW Purdom, J Franco, BW Wah (1999. ) Algorithms for the satisfiability (sat) problem .Handbook of Combinatorial Optimization, , 379 --572
J Franco, M Paull (1983. ) Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem .Discrete Applied Mathematics, , 5 (1 ) ,77 --87
C Ming-Te, J Franco (1990. ) Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiability problem .Information Sciences , , 51 (4 ) ,289 --314
MT Chao, J Franco (1986. ) Probabilistic analysis of two heuristics for the 3-satisfiability problem .SIAM Journal on Computing, , 15 (4 ) ,1106 --1118
J Franco, A Van Gelder (2003. ) A perspective on certain polynomial-time solvable classes of satisfiability .Discrete Applied Mathematics, , 125 (2 ) ,177 --214
JS Schlipf, FS Annexstein, JV Franco, RP Swaminathan (1995. ) On finding solutions for extended Horn formulas .Information Processing Letters, , 54 (3 ) ,133 --137
J. Franco (1986. ) On the probabilistic performance of algorithms for the satisfiability problem .Information Processing Letters , , 23 (2 ) ,103 --106
J. Franco (2001. ) Results related to threshold phenomena research in satisfiability: lower bounds .Theoretical Computer Science, , 265 (1 ) ,147 --157
DS Wise, J Franco (1990. ) Costs of quadtree representation of nondense matrices .Journal of Parallel and Distributed Computing , , 9 (3 ) ,282 --296
J. Franco (1991. ) Elimination of infrequent variables improves average case performance of satisfiability algorithms .SIAM Journal on Computing, , 20 (6 ) ,1119 --1127
J. Franco (1984. ) Probabilistic analysis of the pure literal heuristic for the satisfiability problem .Annals of Operations Research, , 1 (3 ) ,273 --289
K Berman, J Schlipf, J Franco (1995. ) Computing the well-founded semantics faster .Logic Programming and Nonmonotonic Reasoning, , 113 --126
J Franco, J Martin (2009. ) A History of Satisfiability .Handbook of Satisfiability, , 185 ,3 --74
J Franco, M Kouril, J Schlipf, J Ward, S Weaver, M Dransfield, MW Vanfleet (2003. ) SBSAT: a state-based, BDD-based satisfiability solver .International Conference on Theory and Applications of Satisfiability Testing , , 398 --410
J Franco, YC Ho (1988. ) Probabilistic performance of a heuristic for the satisfiability problem .Discrete Applied Mathematics, , 22 (1 ) ,35 --51
V Franco, WM VanFleet, J Schlipf, MR Dransfield (2005. ) Method and system for non-linear state based satisfiability .US Patent 6,912,700, ,
M Kouril, J Franco (2005. ) Resolution tunnels for improved SAT solver performance .International Conference on Theory and Applications of Satisfiability Testing, , 143 --157
LC Murdoch, J Franco (1994. ) The analysis of constant drawdown wells using instantaneous source functions .Water resources research, , 30 (1 ) ,117 --124
J Franco, J Goldsmith, J Schlipf, E Speckenmeyer, RP Swaminathan (1999. ) An algorithm for the class of pure implicational formulas .Discrete Applied Mathematics, , 96 ,89 --106
MN Velev, J Franco (2014. ) Application of constraints to formal verification and artificial intelligence .Ann. Math. Artif. Intell. , , 70 (4 ) ,313 --314
W Yue, J Franco, Q Han, W Cao (2014. ) Improved anytime d* algorithm .IAENG Transactions on Engineering Technologies, , 383 --396
J Franco, S Weaver (2013. ) Algorithms for the Satisfiability Problem .Handbook of Combinatorial Optimization, , 311 --454
Franco J.; Velev M. (01-01-2014. ) Application of constraints to formal verification and artificial intelligence.Annals of Mathematics and Artificial Intelligence, , 70 (4 ) ,313-314 More Information
Yue W.;Franco J.;Han Q.;Cao W. (01-01-2014. ) Improved anytime D*algorithm.Lecture Notes in Electrical Engineering, , 247 LNEE ,383-396 More Information
Franco J.;Weaver S. (01-01-2013. ) Algorithms for the satisfiability problem.Handbook of Combinatorial Optimization, , 1-5 ,311-454 More Information
Yue W.;Franco J.;Cao W.;Han Q. (01-01-2012. ) A new anytime dynamic navigation algorithm .Lecture Notes in Engineering and Computer Science, , 1 ,17-22
Yue W.;Franco J.;Cao W.;Yue H. (06-23-2011. ) ID*Lite: Improved D*Lite algorithm.Proceedings of the ACM Symposium on Applied Computing, , 1364-1369 More Information
Franco J. (03-01-2011. ) Preface to the special issue.Annals of Mathematics and Artificial Intelligence, , 61 (3 ) ,155-157 More Information
Yue W.;Franco J. (11-23-2010. ) A new way to reduce computing in navigation algorithm .Engineering Letters, , 18 (4 ) ,
Franco J.;Martin J. (01-01-2009. ) A history of satisfiability.Frontiers in Artificial Intelligence and Applications, , 185 (1 ) ,3-74 More Information
Franco J. (12-01-2005. ) Typical case complexity of Satisfiability algorithms and the threshold phenomenon.Discrete Applied Mathematics, , 153 (1-3 ) ,89-123 More Information
Creignou N.;Daudé H.;Franco J. (12-01-2005. ) A sharp threshold for the renameable-Horn and the q-Horn properties.Discrete Applied Mathematics, , 153 (1-3 ) ,48-57 More Information
Kouril M.;Franco J. (10-17-2005. ) Resolution tunnels for improved SAT solver performance .Lecture Notes in Computer Science, , 3569 ,143-157
Franco J.;Kouril M.;Schlipf J.;Weaver S.;Dransfield M.;Vanfleet W. (12-01-2004. ) Function-complete lookahead in support of efficient SAT search heuristics .Journal of Universal Computer Science, , 10 (12 ) ,1655-1692
Franco J.;Kouril M.;Schlipf J.;Ward J.;Weaver S.;Dransfield M.;Mark Vanfleet W. (12-01-2004. ) SBSAT: A state-based, BDD-based satisfiability solver .Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), , 2919 ,398-410
Franco J.;Swaminathan R. (08-15-2003. ) On good algorithms for determining unsatisfiability of propositional formulas.Discrete Applied Mathematics, , 130 (2 ) ,129-138 More Information
Franco J.;Van Gelder A. (02-01-2003. ) A perspective on certain polynomial-time solvable classes of satisfiability.Discrete Applied Mathematics, , 125 (2-3 ) ,177-214 More Information
Franco J. (09-03-2001. ) Results related to threshold phenomena research in satisfiability: Lower bounds.Theoretical Computer Science, , 265 (1-2 ) ,147-157 More Information
Franco J. (12-01-2000. ) Some interesting research directions in satisfiability .Annals of Mathematics and Artificial Intelligence, , 28 (1-4 ) ,7-15
Franco J.;Goldsmith J.;Schlipf J.;Speckenmeyer E.;Swaminathan R. (10-15-1999. ) An algorithm for the class of pure implicational formulas.Discrete Applied Mathematics, , 96-97 ,89-106 More Information
Rosenthal J.;Plotkin J.;Franco J. (01-01-1999. ) Probability of pure literals.Journal of Logic and Computation, , 9 (4 ) ,501-513 More Information
Franco J.;Swaminathan R.P. (12-01-1997. ) Average case results for satisfiability algorithms under the random-clause-width model .Annals of Mathematics and Artificial Intelligence, , 20 (1-4 ) ,357-391
Annexstein F.;Franco J. (06-23-1995. ) Work-preserving emulations of shuffle-exchange networks: An analysis of the complex plane diagram.Discrete Applied Mathematics, , 60 (1-3 ) ,13-23 More Information
Berman K.;Franco J.;Schlipf J. (06-23-1995. ) Unique satisfiability of Horn sets can be solved in nearly linear time.Discrete Applied Mathematics, , 60 (1-3 ) ,77-91 More Information
Schlipf J.;Annexstein F.;Franco J.;Swaminathan R. (05-12-1995. ) On finding solutions for extended Horn formulas.Information Processing Letters, , 54 (3 ) ,133-137 More Information
Berman K.A.;Schlipf J.S.;Franco J.V. (01-01-1995. ) Computing the well-founded semantics faster .Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), , 928 ,113-126
Franco J. (02-09-1993. ) On the occurrence of null clauses in random instances of satisfiability.Discrete Applied Mathematics, , 41 (3 ) ,203-209 More Information
Franco J.;Dunn J.;Wheeler W. (03-01-1992. ) Recent work at the interface of logic, combinatorics, and computer science.Annals of Mathematics and Artificial Intelligence, , 6 (1-3 ) ,1-15 More Information
Celis P.;Franco J. (01-01-1992. ) The analysis of hashing with lazy deletions.Information Sciences, , 62 (1-2 ) ,13-26 More Information
Franco J. (01-01-1991. ) Elimination of infrequent variables improves average case performance of satisfiability algorithms.SIAM Journal on Computing, , 20 (6 ) ,1119-1127 More Information
Franco J.;Friedman D. (01-01-1990. ) Towards a facility for lexically scoped, dynamic mutual recursion in Scheme.Computer Languages, , 15 (1 ) ,55-64 More Information
Ming-Te C.;Franco J. (01-01-1990. ) Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k.Information Sciences, , 51 (3 ) ,289-314 More Information
Wise D.;Franco J. (01-01-1990. ) Costs of quadtree representation of nondense matrices.Journal of Parallel and Distributed Computing, , 9 (3 ) ,282-296 More Information
Franco J.;Friedman D.;Johnson S. (01-01-1990. ) Multi-way streams in Scheme.Computer Languages, , 15 (2 ) ,109-125 More Information
Franco J.;Friedman D. (01-01-1989. ) Creating efficient programs by exchanging data for procedures.Computer Languages, , 14 (1 ) ,11-23 More Information
Franco J.;Ho Y. (01-01-1988. ) Probabilistic performance of a heuristic for the satisfiability problem.Discrete Applied Mathematics, , 22 (1 ) ,35-51 More Information
Franco J.;Plotkin J.;Rosenthal J. (01-01-1987. ) Correction to probabilistic analysis of the Davis Putnam procedure for solving the satisfiability pr.Discrete Applied Mathematics, , 17 (3 ) ,295-299 More Information
Franco J. (08-20-1986. ) On the probabilistic performance of algorithms for the satisfiability problem.Information Processing Letters, , 23 (2 ) ,103-106 More Information
Choukhmane E.; Franco J. (01-01-1986. ) An approximation algorithm for the maximum independent set problem in cubic planar graphs.Networks, , 16 (4 ) ,349-356 More Information
Chao M.;Franco J. (01-01-1986. ) PROBABILISTIC ANALYSIS OF TWO HEURISTICS FOR THE 3-SATISFIABILITY PROBLEM.SIAM Journal on Computing, , 15 (4 ) ,1106-1118 More Information
Franco J. (10-01-1984. ) Probabilistic analysis of the pure literal heuristic for the satisfiability problem.Annals of Operations Research, , 1 (3 ) ,273-289 More Information
Franco J.;Paull M. (01-01-1983. ) Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem.Discrete Applied Mathematics, , 5 (1 ) ,77-87 More Information
Book Chapter
J Franco and S. Weaver (2013 ) Algorithms for the Satisfiability Problem Handbook on Combinatorial Optimization .(pp. 311 --454).Springer (Author)
J. Franco (2010 ) Probabilistic analysis of Satisfiability algorithms Boolean Methods and Models .
J. Franco and J. Martin (2009 ) A History of Satisfiability Handbook on Satisfiability .IOS Press
J. Gu, P.W. Purdom, J. Franco, and B.W. Wah (2002 ) Algorithms for the Satisfiability (SAT) Problem Handbook of Applied Optimization .(pp. 640 --660).Oxford University Press
J. Gu, P.W. Purdom, J. Franco, and B. Wah (1999 ) Algorithms for the Satisfiability (SAT) Problem Handbook of Combinatorial Optimization, Supplement Volume A .Kluwer
Other Information
https://scholar.google.com/citations?user=ldgiV80AAAAJ&hl=en&oi=ao,