stanford-oval/wikipedia huggingface dataset:
Các phương pháp hình thức

Trong ngành khoa học máy tính, các phương pháp hình thức là các kỹ thuật toán học cho việc đặc tả, phát triển và kiểm định các hệ thống phần mềm và phần cứng. Cách tiếp cận này đặc biệt quan trọng đối với các hệ thống cần có tính toàn vẹn cao, chẳng hạn hệ thống điều khiển lò phản ứng hạt nhân hay điều khiển tên lửa, khi an toàn hay an ninh có vai trò quan trọng, để góp phần đảm bảo rằng quá trình phát triển hệ thống sẽ không có lỗi. Các phương pháp hình thức đặc biệt hiệu quả tại giai đoạn đầu của quá trình phát triển (tại các mức yêu cầu và đặc tả hệ thống), nhưng cũng có thể được sử dụng cho một quá trình phát triển hoàn chỉnh của một hệ thống.
Phân loại

Các phương pháp hình thức có thể được sử dụng tại nhiều mức:
Mức 0: Đặc tả hình thức có thể được thực hiện và rồi một chương trình được phát triển từ đặc tả này một cách không hình thức. Trong nhiều trường hợp, cách này có thể là lựa chọn hiệu quả nhất về mặt chi phí.
Mức 1: Sử dụng phát triển và kiểm định hình thức để tạo một chương trình theo một quy trình hình thức hơn. Ví dụ, có thể thực hiện các chứng minh về các tính chất hoặc quá trình tinh chỉnh (refinement) từ đặc tả hình thức tới một chương trình. Đây có thể là lựa chọn phù hợp nhất đối với các hệ thống yêu cầu tính toàn vẹn cao với các tiêu chí về an toàn và an ninh.
Mức 2: Sử dụng các bộ chứng minh định lý (theorem prover) để thực hiện các chứng minh hình thức hoàn toàn và được kiểm chứng bằng máy móc. Việc này có thể đòi hỏi chi phí rất cao và chỉ đáng lựa chọn trong thực tiễn nếu phí tồn cho các lỗi sai là cực kỳ cao (ví dụ, trong các phần quan trọng của thiết kế bộ vi xử lý).
Cùng với ngành con Ngữ nghĩa hình thức của ngôn ngữ lập trình, các phương pháp hình thức có thể được phân loại tương đối như sau:
Ngữ nghĩa ký hiệu (Denotational semantics), trong đó ý nghĩa của một hệ thống được biểu diễn bằng lý thuyết toán học về miền xác định. Lợi điểm của những phương pháp này phụ thuộc vào bản chất được hiểu rõ của các miền xác định để từ đó đem lại ý nghĩa cho hệ thống; các phê phán chỉ ra rằng không phải hệ thống nào cũng có thể được nhìn một cách tự nhiên hoặc trực quan dưới dạng một hàm số.
Ngữ nghĩ hoạt động (Operational semantics), trong đó, ý nghĩa của một hệ thống được biểu diễn bằng một chuỗi các hành động của một mô hình tính toán (giả thiết là) đơn giản hơn. Lợi điểm của phương pháp này là tính đơn giản của các mô hình tạo nên sự trong sáng của biểu diễn; nhược điểm là phương pháp này đã trì hoãn các vấn đề của ngữ nghĩa (ai định nghĩa ngữ nghĩa của các mô hình đơn giản hơn?)
Ngữ nghĩa tiên đề (Axiomatic semantics), trong đó ý nghĩa của hệ thống được biểu diễn theo các tiền điều kiện (precondition) và hậu điều kiện (postcondition), đây lần lượt là các điều kiện phải được thỏa mãn tại các thời điểm trước và sau khi hệ thống thực hiện một nhiệm vụ. Những người ủng hộ phương pháp này nói đến mối quan hệ của nó với lôgic kinh điển; những người phê phán nói rằng những ngữ nghĩa thuộc dạng này không thực sự mô tả xem hệ thống làm cái gì (chỉ là cái gì đúng trước đó và sau đó).
Sử dụng

Các phương pháp hình thức có thể được áp dụng tại nhiều điểm khác nhau trong cả quá trình phát triển phần mềm. (Tuy có thể nói đến một quá trình phát triển bất kỳ, để thuận tiện, ta sẽ dùng các thuật ngữ của mô hình thác nước).
Sử dụng > Đặc tả

Các phương pháp hình thức có thể được sử dụng để mô tả về hệ thống cần phát triển, tại bất kỳ mức độ chi tiết nào mà ta muốn. Mô tả hình thức này có thể được sử dụng để hướng dẫn các hoạt động phát triển tiếp theo (xem các mục dưới); ngoài ra, nó có thể được sử dụng để kiểm định xem các yêu cầu cho hệ thống đang được phát triển đã được đặc tả một cách đầy đủ và chính xác hay chưa.
Nhu cầu về các hệ thống đặc tả hình thức đã được nói đến từ nhiều năm. Trong Báo cáo ALGOL 60, John Backus đã trình bày một hệ thống ký hiệu hình thức để mô tả cú pháp ngôn ngữ lập trình (sau này được đặc tên là Backus normal form hay Backus-Naur form (BNF) (Dạng chuẩn tắc Backus));
Sử dụng > Phát triển

Khi một đặc tả hình thức đã được phát triển xong, đặc tả đó có thể được sử dụng làm một hướng dẫn trong quá trình hệ thống thực được phát triển (nghĩa là được hiện thực hóa trong phần mềm và/hoặc phần cứng). Ví dụ:
Nếu đặc tả hình thức là một ngữ nghĩa hoạt động, hành vi được quan sát của hệ thống thực sẽ có thể được so sánh với hành vi trong đặc tả (chính đặc tả cũng nên chạy được hoặc giả lập được). Thêm vào đó, các lệnh hoạt động của đặc tả có thể thích hợp cho việc dịch thẳng mã chạy được.
Nếu đặc tả hình thức là một ngữ nghĩa tiên đề, các tiền điều kiện và hậu điều kiện của đặc tả có thể trở thành các assertion
If the formal specification is in an axiomatic semantics, the preconditions and postconditions of the specification may become khẳng định (assertion') trong mã chạy được.
Sử dụng > Kiểm định

Khi một đặc tả hình thức đã được phát triển, đặc tả này có thể được dùng làm cơ sở cho việc chứng minh các tính chất của đặc tả.
Sử dụng > Kiểm định > Chứng minh của con người

Đôi khi, động cơ cho việc chứng minh tính đúng đắn của một hệ thống không phải là nhu cầu đảm bảo tính đúng đắn của hệ thống mà là mong muốn hiểu rõ hơn về hệ thống. Do đó, một số chứng minh được thực hiện dưới hình thức chứng minh toán học: viết tay hoặc đánh máy nội dung bằng ngôn ngữ tự nhiên, với mức độ phi hình thức như các chứng minh toán học thông thường mà con người vẫn thực hiện. Một chứng minh "tốt" là một chứng minh mà những người khác có thể đọc được và hiểu được.
Các phê phán đối với cách tiếp cận này nói rằng tính đa nghĩa cố hữu trong ngôn ngữ tự nhiên cho phép các lỗi sai trong các chứng minh đó có thể không bị phát hiện; nhiều khi, những lỗi tinh vi có thể xuất hiện trong các chi tiết mức thấp mà thường không được để ý đến bởi những chứng minh thuộc kiểu này. Ngoài ra, việc tạo ra các chứng minh tốt đòi hỏi trình độ toán học cao.
Sử dụng > Kiểm định > Chứng minh tự động

Ngược lại, ngày càng có nhiều quan tâm đến các chứng minh về tính đúng đắn của hệ thống bằng các phương tiện tự động. Các kỹ thuật tự động được phân thành hai loại chính:
Chứng minh định lý tự động, trong đó, khi cho trước một mô tả về hệ thống, một tập các tiên đề lôgic và một tập các quy tắc suy luận, một hệ thống sẽ cố gắng tự xây dựng một chứng minh hình thức từ đầu.
Kiểm tra mô hình, trong đó, một hệ thống kiểm định các tính chất nhất định bằng cách duyệt trong toàn bộ tất cả các trạng thái mà trong thời gian chạy, hệ thống có thể vào trạng thái đó.
Cả hai kỹ thuật trên đều hoạt động mà không cần đến sự hỗ trợ của con người. Các bộ chứng minh định lý tự động thường yêu cầu định hướng xem các tính chất nào là đáng quan tâm; các bộ kiểm tra mô hình có thể nhanh chóng sa lầy vào việc kiểm tra hàng triệu trạng thái không đáng quan tâm nếu không được cho trước một mô hình đủ trừu tượng.
Những người ủng hộ các hệ thống này cho rằng các kết quả của chúng có độ xác tính toán học cao hơn các chứng minh của con người, do tất cả các chi tiết buồn tẻ đã được kiểm định một cách có thuật toán. Việc huấn luyện cần thiết để có thể sử dụng được các hệ thống này cũng ít hơn đòi hỏi cần thiết cho việc tạo ra các chứng minh toán học tốt bằng tay. Nhờ đó, các kỹ thuật này có thể dùng được cho nhiều người hơn.
Những người phê phán cho rằng các hệ thống kiểu này giống như máy sấm truyền: chúng đưa ra các tuyên bố về sự thật nhưng lại không đưa ra giải thích nào về sự thực đó. Còn có cả vấn đề "kiểm định hệ kiểm định"; nếu chính chương trình tham gia công tác kiểm định không được chứng minh là đúng, thì có thể có lý do để nghi ngờ tính đúng đắn của các kết quả được tạo ra.
Phê phán

Bên cạnh các phê phán nội bộ nói trên, còn có các phê phán dành cho toàn bộ ngành các phương pháp hình thức. Với tầm phát triển hiện nay, các chứng minh về tính đúng đắn, bằng tay hoặc bằng máy tính, đòi hỏi nhiều thời gian (và do đó cả tiền bạc) để được tạo ra, với lợi ích hạn chế ngoài việc đảm bảo tính đúng đắn. Điều đó làm cho các phương pháp hình thức thường chỉ được dùng trong các lĩnh vực thu được lợi ích từ việc có được các chứng minh đó, hoặc sẽ gặp nguy hiểm nếu có các lỗi không được phát hiện. Ví dụ, trong kỹ thuật hàng không, các lỗi không được phát hiện có thể gây chết chóc, do đó các phương pháp hình thức được dùng rộng rãi trong ngành này hơn trong các lĩnh vực ứng dụng khác.
Các phương pháp hình thức và hệ thống ký hiệu

Abstract State Machines (ASMs)
Alloy
B-Method
Process calculi
CSP
π-calculus
Actor model
Esterel
Lustre
Petri nets
RAISE
VDM
Z notation
Epicauta leucocoma

| Epicauta leucocoma> Phân loại khoa học |
| --- | --- |
Giới (regnum): Animalia
Ngành (phylum): Arthropoda
Lớp (class): Insecta
Bộ (ordo): Coleoptera
Họ (familia): Meloidae
Chi (genus): Epicauta
Loài (species): E. leucocoma
Danh pháp hai phần
Epicauta leucocoma Champion, 1892 
Epicauta leucocoma là một loài bọ cánh cứng trong họ Meloidae. Loài này được Champion mô tả khoa học năm 1892.
Chú thích

↑  Meloidae in Synopsis of the described Coleoptera of the World 6 juni 2010
Clavus mighelsi

| Clavus mighelsi> Phân loại khoa học |
| --- | --- |
Giới (regnum): Animalia
Ngành (phylum): Mollusca
Lớp (class): Gastropoda
Liên họ (superfamilia): Conoidea
(không phân hạng): nhánh Caenogastropoda nhánh Hypsogastropoda nhánh Neogastropoda
Họ (familia): Drilliidae
Chi (genus): Clavus
Loài (species): C. mighelsi
Danh pháp hai phần
Clavus mighelsi Kay, 1979 
Danh pháp đồng nghĩa
 Clavus (Tylotiella) mighelsi Kay, 1979
Clavus mighelsi là một loài ốc biển, là động vật thân mềm chân bụng sống ở biển trong họ Drilliidae.
Chú thích

↑  Clavus mighelsi Kay, 1979. World Register of Marine Species, truy cập 5 tháng 4 2010.
Colobothea peruviana

| Colobothea peruviana> Phân loại khoa học |
| --- | --- |
Giới (regnum): Animalia
Ngành (phylum): Arthropoda
Lớp (class): Insecta
Bộ (ordo): Coleoptera
Phân bộ (subordo): Polyphaga
Liên họ (superfamilia): Cerambycoidea
Họ (familia): Cerambycidae
Chi (genus): Colobothea
Loài (species): C. peruviana
Danh pháp hai phần
Colobothea peruviana Aurivillius, 1920 
Colobothea peruviana là một loài bọ cánh cứng trong họ Cerambycidae.
Chú thích

↑  Bisby, F.A.; Roskov, Y.R.; Orrell, T.M.; Nicolson, D.; Paglinawan, L.E.; Bailly, N.; Kirk, P.M.; Bourgoin, T.; Baillargeon, G.; Ouvrard, D. (2011). “Species 2000 & ITIS Catalogue of Life: 2011 Annual Checklist”. Species 2000: Reading, UK. Truy cập ngày 24 tháng 9 năm 2012.
Eilema vicaria

| Eilema vicaria> Phân loại khoa học |
| --- | --- |
Giới (regnum): Animalia
Ngành (phylum): Arthropoda
Lớp (class): Insecta
Bộ (ordo): Lepidoptera
Họ (familia): Erebidae
Chi (genus): Eilema
Loài (species): E. vicaria
Danh pháp hai phần
Eilema vicaria
Eilema vicaria là một loài bướm đêm thuộc phân họ Arctiinae, họ Erebidae.
Chú thích

↑  Bisby, F.A.; Roskov, Y.R.; Orrell, T.M.; Nicolson, D.; Paglinawan, L.E.; Bailly, N.; Kirk, P.M.; Bourgoin, T.; Baillargeon, G.; Ouvrard, D. (2011). “Species 2000 & ITIS Catalogue of Life: 2011 Annual Checklist”. Species 2000: Reading, UK. Truy cập ngày 24 tháng 9 năm 2012.
Cầu thủ xuất sắc nhất năm 2000 của FIFA

Giải thưởng Cầu thủ xuất sắc nhất năm 2000 của FIFA được trao cho cầu thủ Zinedine Zidane. Đây cũng là lần thứ hai anh vinh dự nhận danh hiệu cá nhân cao quý này. Cũng trong năm này, Zinedine Zidane cung đội tuyển Pháp giành được chức Vô địch Euro 2000.
Kết quả

| Xếp hạng | Cầu thủ | Điểm | Câu lạc bộ |
| --- | --- | --- | --- |
| 1 |  Zinedine Zidane | 370 |  Juventus |
| 2 |  Luís Figo | 329 |  FC Barcelona →  Real Madrid |
| 3 |  Rivaldo | 263 |  FC Barcelona |
| 4 |  Gabriel Batistuta | 57 |  ACF Fiorentina →  AS Roma |
| 5 |  Andriy Shevchenko | 48 |  AC Milan |
| 6 |  David Beckham | 41 |  Manchester United |
| 7 |  Thierry Henry | 35 |  Arsenal F.C. |
| 8 |  Alessandro Nesta | 23 |  AC Milan |
| 9 |  Patrick Kluivert | 22 |  FC Barcelona |
| 10 |  Francesco Totti | 14 |  AS Roma |
| 11 |  Raúl | 12 |  Real Madrid |
Danh sách phố ma tại Hoa Kỳ

Đây là danh sách các phố ma tại Hoa Kỳ. Đó là những thị trấn nhỏ vẫn còn dân sinh sống, song dân số đã giảm đáng kể khiến thị trấn trở nên vắng vẻ. Có những phố ma ở Hoa Kỳ hoang vắng đến mức cây cối mọc rậm rạp che mất lối vào và nguy hiểm.
Bodie, California
Bannack, Montana
Animas Forks, Colorado
St. Elmo trong quận Chaffee, tiểu bang Colorado
Kennicott, Alaska
Danh sách các phố ma theo tiểu bang > Alabama

Bài chi tiết: Danh sách phố ma tại Alabama
Danh sách các phố ma theo tiểu bang > Alaska

Cape York
Council
Dyea
Iditarod
Independence Mine
Katalla
Kennicott
Kern
King Island
Knik
Mary's Igloo
Ohagamiut
Ophir
Prospect Creek
Seaside
Snettisham
Speel River
Three Saints Bay
Danh sách các phố ma theo tiểu bang > Arizona

Bài chi tiết: Danh sách phố ma tại Arizona
Danh sách các phố ma theo tiểu bang > Arkansas

Bài chi tiết: Danh sách phố ma tại Arkansas
Danh sách các phố ma theo tiểu bang > California

Bài chi tiết: Danh sách phố ma tại California
Danh sách các phố ma theo tiểu bang > Colorado

Bài chi tiết: Danh sách phố ma tại Colorado
Danh sách các phố ma theo tiểu bang > Connecticut

Bara-Hack
Cuties Island
Dudleytown
Gay City
Little People Village
Pleasure Beach
Danh sách các phố ma theo tiểu bang > Delaware

Banning
Glenville
New Market
Owens Station
Saint Johnstown
Zwaanendael (khu định cư đầu tiên trong tiểu bang)
Danh sách các phố ma theo tiểu bang > Florida

Acron, Florida
Acton, Florida
Allenhurst, Florida
Andytown, Florida
Anona, Florida
Aurytown, Florida
Bareah, Florida
Barrsville, Florida
Basinger, Florida
Bay Harbor, Florida
Bayport, Florida
Bayview, Florida
Bethany, Florida
Birdon, Florida
Brewster, Florida
Bullowville, Florida
Bunkerhill, Florida
Castor Town, Florida
Centralia, Florida
Campville, Florida
Chicora, Florida
Citrus Center, Florida
College Hill, Florida
Columbus, Florida
Cornwell, Florida
Cosme, Florida
Crewsville, Florida
Cromanton, Florida
Croom, Florida
East Goose Creek, Florida
Edgeville, Florida
Eldora, Florida
Ellaville, Florida
Fivay, Florida
Flamingo, Florida
Fontaine, Florida
Fort Brooke, Florida
Fort Chokonikla, Florida
Fort Dade, Florida
Fort Dallas, Florida
Fort Desoto, Florida
Fort Drum, Florida
Fort Jefferson, Florida
Fort King, Florida
Fort Kissimmee, Florida
Fort Lonesome, Florida
Fort Mose, Florida
Gaiter, Florida
Garfield, Florida
Goodno, Florida
Green Pond, Florida
Gulf City, Florida
Hague, Florida
Hall City, Florida
Hampton Springs, Florida
Heidtville, Florida
Hicora, Florida
Hopewell, Florida
Hopkins, Florida
Indian Key, Florida
Indian River City, Florida
Island Grove, Florida
Jane Jay, Florida
Juliette, Florida
Kenansville, Florida
Kerr City, Florida
Kicco, Florida
Kismet, Florida
Koreshan, Florida
Kreamer Island, Florida
Lake Fern, Florida
Leno, Florida
Liverpool, Florida
Lulu, Florida
Magnolia, Florida
Manasota, Florida
Manhattan, Florida
Mannfield, Florida
Mars, Florida
Midland, Florida
Montbrook, Florida
Muscogee, Florida
Negro Fort, Florida
New Troy, Florida
Newnansville, Florida
Old Bethel, Florida
Old California, Florida
Old Venus, Florida
Orsino, Florida
Parmalee, Florida
Parramore, Florida
Pembroke, Florida
Perky, Florida
Peru, Florida
Picnic, Florida
Picture City, Florida
Pigeon Key
Pine Level, Florida
Pittman, Florida
Port Leon, Florida
Port Tampa, Florida
Punta Rassa, Florida
Rattlesnake, Florida
Ringgold, Florida
Rochelle, Florida
Romeo, Florida
Rosewood, Florida
Runnymede, Florida
Rye, Florida
Sandy, Florida
Sardis, Florida
Sherman, Florida
Sisco, Florida
Slighville, Florida
Spray, Florida
St. Francis, Florida
St. Joseph, Florida
Stage Pond, Florida
Stanton, Florida
Stiltsville, Florida
Sulphur Springs, Florida
Sumica, Florida
Sun City, Florida
Tasmania, Florida
Tillman, Florida
Torrey, Florida
Traxler, Florida
Troy, Florida
Vandolah, Florida
Verna, Florida
Vicksburg, Florida
Villa City, Florida
Waterbury, Florida
Welchton, Florida
Welcome, Florida
West Tocoi, Florida
Willow, Florida
Wilson, Florida
Yamato Colony, Florida
Danh sách các phố ma theo tiểu bang > Georgia

Allatoona
Auraria
Campbellton
Ceney
Chestatee
Chubbtown
Creighton
Diamond
Doctortown
Ebenezer
Ehpesus
Esom Hill
Everett Springs
Felton
Harnageville (còn được biết đến với tên Tate)
Holland
Jacksonboro
Knucklesville
Livingston
Marblehill
McWorther
Mountain View
Plunkett Town
PoBiddy Crossroads
Possum Trot
Scull Shoals
Sixes
Spring Place
Tilton
Tyus
Wax
Danh sách các phố ma theo tiểu bang > Hawaii

Apua
Kaimu
Kalapana
Kapoho
Mana
Waialee
Danh sách các phố ma theo tiểu bang > Idaho

Bayhorse
Bonanza
Burke
Cobalt
Comeback Mining Camp
Custer
De Lamar
Florence
Gilmore
Golden Age camp
Idaho City
Leesburg
Mount Idaho
Placerville
Rocky Bar
Ruby City
Sawtooth City
Silver City
Strevell
Vienna
Yellow Jacket
Danh sách các phố ma theo tiểu bang > Illinois

Anderson
Barr
Benjaminville
Brush Point
Bybee
Cardiff
Challacombe
Clayville
Clifford Eight
Coltonville
Comer
Enos
Evans
Greenridge
Green Rock
Griggsville Landing
Hagaman
Horace
Kankakee City
Kaskaskia (cựu thủ phủ tiểu bang)
Kumler
Ledford
Lemmon
Macoupin
McVey
Miles Station
Millsdale
Morse
Muddy
Old Evansville
Old Westville
Orchard Place
Papsville
Parker City
Reeders
Riverview
Rodden
Santa Fe Park
Schoper
Stanchnikville
Vishnu Springs
Weston, Quận Kane
Womac
Danh sách các phố ma theo tiểu bang > Indiana

Baltimore
Beeville
Brisco
Chatterton
Chesapeake
Collins
Corwin (Quận Henry)
Corwin (Quận Tippecanoe)
Elkinsville
Glen Hall
Granville
Heath
Kickapoo
Locust Grove
Monument City (Quận Huntington)
Point Pleasant
Quaker
Randall
Sheff
Sloan
Toronto
Tremont
Walnut Grove
Warrenton
Danh sách các phố ma theo tiểu bang > Iowa

Bryantsburg
Buxton
Buchanan
Conover
Donnan
Doris
Dudley
Elkport
Green Island
Littleport
Motor
National
Shady Grove
Siegel
Danh sách các phố ma theo tiểu bang > Kansas

Bài chi tiết: Danh sách phố ma tại Kansas
Danh sách các phố ma theo tiểu bang > Kentucky

Blue Heron
Creelsboro
Fudge
Paradise
Scuffletown
Danh sách các phố ma theo tiểu bang > Louisiana

East Krotz Springs
Elliot City
Waterloo
Ruddock
Danh sách các phố ma theo tiểu bang > Maine

Flagstaff (Chìm dưới nước tạo thành  Flagstaff Lake)
Perkins Township (Swan Island)
Danh sách các phố ma theo tiểu bang > Maryland

Broad Creek
Collington
Lapidum
Sinepuxent
Wagner's Point
Danh sách các phố ma theo tiểu bang > Massachusetts

Catamount
Dana (Chìm dưới nước tạo thành  Quabbin Reservoir)
Davis
Dogtown
Enfield (Chìm dưới nước tạo thành  Quabbin Reservoir)
Greenwich (Chìm dưới nước tạo thành  Quabbin Reservoir)
North Bridgewater (located in between the current towns of West Bridgewater và Brockton)
Prescott (Chìm dưới nước tạo thành  Quabbin Reservoir)
Danh sách các phố ma theo tiểu bang > Michigan

Xem Danh sách phố ma tại Michigan.
Danh sách các phố ma theo tiểu bang > Minnesota

Xem Danh sách phố ma tại Minnesota.
Danh sách các phố ma theo tiểu bang > Mississippi

Bankston
Brewton
Camargo
Cotton Gin Port
Gainesville
Holmesville
Napoleon
Rocky Springs
Rodney
Wontierioniasiopolis
Woolworth
Danh sách các phố ma theo tiểu bang > Missouri

Arlington
Bloodland
Cookville
Goldman
Hamburg
Howell
Monark Springs
Possum Trot
Saint Annie
Times Beach
Toonerville
Wayman
Xenia
(Note: Hamburg, Howell, and Toonerville were all located in Quận St. Charles, Missouri.  All three towns became part of the Weldon Spring Ordnance Works in 1941 for WWII, which later became part of the Weldon Spring Site Remedial Action Project (WSSRAP))
Danh sách các phố ma theo tiểu bang > Montana

Aldridge
Alton
Argo
Bannack
Barker
Bean
Bear Creek
Bearmouth
Bowler
Cable
Carter
Castle City
Coburg
Coloma
Comertown
Comet
Coolidge
Corwin
Dooley
Electric
Elkhorn
Ewing
Exeter
Fox
Garnet
Giltedge
Glendale
Gold Creek
Granite
Hassel
Hecla
Hillsboro
Independence
Ingomar
Jardine
Kendall
Keystone
Kirkville
Landusky
Laurin
Lonetree
Maiden
Mammoth
Marysville
Maudlow
Melrose
Nevada City
Old Chico
Pardee
Pioneer, Quận Beaverhead
Pioneer, Quận Powell
Pony
Red Bluff
Red Lion
Rimini
Rockvale
Ruby
Ruby Gulch
Silesia
Silver Bow
Sixteen
Southern Cross
Stark
Storrs
Sumatra
Taft
Thoeny
Tower
Vananda
Vandalia
Virginia City
Washoe
Wagner
Wickes
Zortman
Danh sách các phố ma theo tiểu bang > Nebraska

Breslau
De Soto
DeWitty
Dobytown
Duff
Omadi
Pittsburg
Rock Bluff
Spring Ranche
Danh sách các phố ma theo tiểu bang > Nevada

Bài chi tiết: Danh sách phố ma tại Nevada
Danh sách các phố ma theo tiểu bang > New Hampshire

Beebe River
Livermore
Monson
Danh sách các phố ma theo tiểu bang > New Jersey

Batsto Village (là một phố ma nhưng sau đó được biến đổi thành một bảo tàng ngoài trời)
Deserted Village
Double Trouble
Quận Island Beach
Ong's Hat
Port Elizabeth (không nên nhầm lẫn với Elizabethport)
Raritan Landing
South Cape May+
Whitesbog Village
Danh sách các phố ma theo tiểu bang > New Mexico

Baldy Town
Blackdom
Bland
Cabezon
Chloride
Clairmont
Cooney
Dawson
El Ojo Del Padre
Elizabethtown
Hermosa
Gage
Gobernador
Gran Quivira (now part of the Salinas Pueblo Missions National Monument)
Lake Valley
Mentmore  (still has post office and zip code 87319)
Mogollon
Mowry
Pinos Altos (High Pines). Still has some people there, located near Silver City
Pittsburg
Red Hill
Santa Rita
Shakespeare
Steins
Tyrone
Vinegaroon (East of La Luz, Otero Co., at the mouth of La Borcita)
Danh sách các phố ma theo tiểu bang > New York

Doodletown
Tahawus
Conklinville (Under Great Sacandaga Lake)
Love Canal
Danh sách các phố ma theo tiểu bang > North Carolina

Buffalo City
Brunswick Town (former state capital)
Cataloochee
Diamond City
Judson (Under Fontana Lake)
Portsmouth
Roanoke Colony
Whitney Town, Quận Stanly, North Carolina (partially submerged by Badin Lake)
Danh sách các phố ma theo tiểu bang > North Dakota

Alfred
Aurelia
Bently
Brisbane
Charbonneau
Churchs Ferry
Dogtooth.
Fort Buford
Hartland
Heaton
Leipzig
Lonetree
Melville
Omeemee
Petrel
Sims
Tagus
Temple
Temvik
Van Hook
Verendrye
Wheelock
Danh sách các phố ma theo tiểu bang > Ohio

Ai
Atwood - Thị trấn nhỏ trong miền nam Quận Summit.
Atwood - Thị trấn nhỏ trong Quận Carroll. Bị bỏ hoang để nhường chỗ cho Hồ Atwood trong nỗ lực kiểm soát lũ lụt
Blowville
Blue Ball
Claylick, Quận Licking, Ohio nằm tại giao điểm của Claylick và sông Licking. Từng là một trong các thị trấn lớn nhất bị tàn phá, chính yếu bởi hai trận lụt năm 1919 và năm 1959. Sau trận lụt thứ hai, dự án Đập Dillan được tiến hành và phá hủy thị trấn.
Elk Lick (Bị tàn phá và cho ngập nước sau khi xây Hồ William H. Harsha)
Boston còn gọi là. "Helltown"
Hibernia
Ingham
Knockemstiff
Moonville
New Burlington
New Hampton
Newville
Oreton
Providence
Revenge
Rumley
Rural Hill (Từng là thị trấn thịnh vượng nhưng bỏ hoang sau khi lò mổ địa phương (nơi mướn nhiều công nhân) đóng cửa)
San Toy
Tadmor
Sprucevale  (Thị trấn kênh bị bỏ hoang năm 1870 sau khi kênh đóng cửa. Các âu thuyền của kênh này vẫn còn tồn tại ngày nay)
Utopia
Winchester
Wonderland